Session Gale_Shapley
View
theory dependencies
View
document
View
outline
Theories
HOL-Hoare.Hoare_Syntax
File ‹hoare_syntax.ML›
HOL-Hoare.Hoare_Tac
File ‹hoare_tac.ML›
HOL-Hoare.Hoare_Logic
List-Index.List_Index
HOL-Library.While_Combinator
HOL-Library.LaTeXsugar
Gale_Shapley1
HOL-Library.AList
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›
Automatic_Refinement.Misc
Automatic_Refinement.Foldi
Collections.SetIterator
Collections.SetIteratorOperations
Collections.Assoc_List
Automatic_Refinement.Refine_Util_Bootstrap1
Automatic_Refinement.Mpat_Antiquot
Automatic_Refinement.Mk_Term_Antiquot
Automatic_Refinement.Refine_Util
Automatic_Refinement.Attr_Comb
Automatic_Refinement.Named_Sorted_Thms
Automatic_Refinement.Prio_List
Automatic_Refinement.Tagged_Solver
Automatic_Refinement.Anti_Unification
Automatic_Refinement.Indep_Vars
Automatic_Refinement.Select_Solve
Automatic_Refinement.Mk_Record_Simp
Automatic_Refinement.Refine_Lib
File ‹Cond_Rewr_Conv.ML›
File ‹Revert_Abbrev.ML›
Automatic_Refinement.Relators
Automatic_Refinement.Param_Tool
Automatic_Refinement.Param_HOL
Automatic_Refinement.Parametricity
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
HOL-Library.Code_Target_Numeral
Collections.Diff_Array
Gale_Shapley2