Session Dict_Construction
View
theory dependencies
View
document
View
outline
Theories
Introduction
Impossibility
Automatic_Refinement.Refine_Util_Bootstrap1
Automatic_Refinement.Mpat_Antiquot
Automatic_Refinement.Mk_Term_Antiquot
Automatic_Refinement.Refine_Util
Dict_Construction
File ‹dict_construction_util.ML›
File ‹transfer_termination.ML›
File ‹congruences.ML›
File ‹side_conditions.ML›
File ‹class_graph.ML›
File ‹dict_construction.ML›
Termination
HOL-Library.ListVector
Test_Dict_Construction
Test_Side_Conditions
Lazy_Case.Lazy_Case
File ‹lazy_case.ML›
Deriving.Generator_Aux
File ‹bnf_access.ML›
File ‹generator_aux.ML›
Deriving.Derive_Manager
File ‹derive_manager.ML›
Show.Show
File ‹show_generator.ML›
Show.Show_Instances
Test_Lazy_Case