Session Automatic_Refinement
View
theory dependencies
View
document
View
outline
Theories
Refine_Util_Bootstrap1
Mpat_Antiquot
Mk_Term_Antiquot
Refine_Util
Attr_Comb
Named_Sorted_Thms
Prio_List
Tagged_Solver
Anti_Unification
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
HOL-ex.Quicksort
HOL-Library.Option_ord
HOL-Library.Infinite_Set
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Misc
Foldi
Indep_Vars
Select_Solve
Mk_Record_Simp
Refine_Lib
File ‹Cond_Rewr_Conv.ML›
File ‹Revert_Abbrev.ML›
Param_Chapter
Relators
Param_Tool
Param_HOL
Parametricity
Autoref_Phases
Autoref_Data
Autoref_Tagging
Autoref_Id_Ops
Autoref_Fix_Rel
Autoref_Relator_Interface
Autoref_Translate
Autoref_Gen_Algo
Autoref_Chapter
Autoref_Tool
Autoref_Bindings_HOL
Automatic_Refinement