author | blanchet |
Tue, 16 Sep 2014 19:23:37 +0200 | |
changeset 58352 | 37745650a3f4 |
parent 57959 | 1bfed12a7646 |
child 58816 | aab139c0003f |
permissions | -rw-r--r-- |
(* Title: HOL/Fun_Def_Base.thy Author: Alexander Krauss, TU Muenchen *) header {* Function Definition Base *} theory Fun_Def_Base imports Ctr_Sugar Set Wellfounded begin ML_file "Tools/Function/function_lib.ML" named_theorems termination_simp "simplification rules for termination proofs" ML_file "Tools/Function/function_common.ML" ML_file "Tools/Function/context_tree.ML" setup Function_Ctx_Tree.setup ML_file "Tools/Function/sum_tree.ML" end