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