1(* Title: HOL/Fun_Def_Base.thy 2 Author: Alexander Krauss, TU Muenchen 3*) 4 5section \<open>Function Definition Base\<close> 6 7theory Fun_Def_Base 8imports Ctr_Sugar Set Wellfounded 9begin 10 11ML_file "Tools/Function/function_lib.ML" 12named_theorems termination_simp "simplification rules for termination proofs" 13ML_file "Tools/Function/function_common.ML" 14ML_file "Tools/Function/function_context_tree.ML" 15 16attribute_setup fundef_cong = 17 \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close> 18 "declaration of congruence rule for function definitions" 19 20ML_file "Tools/Function/sum_tree.ML" 21 22end 23