equal
deleted
inserted
replaced
6 |
6 |
7 theory Fun_Def_Base |
7 theory Fun_Def_Base |
8 imports Ctr_Sugar Set Wellfounded |
8 imports Ctr_Sugar Set Wellfounded |
9 begin |
9 begin |
10 |
10 |
11 ML_file "Tools/Function/function_lib.ML" |
11 ML_file \<open>Tools/Function/function_lib.ML\<close> |
12 named_theorems termination_simp "simplification rules for termination proofs" |
12 named_theorems termination_simp "simplification rules for termination proofs" |
13 ML_file "Tools/Function/function_common.ML" |
13 ML_file \<open>Tools/Function/function_common.ML\<close> |
14 ML_file "Tools/Function/function_context_tree.ML" |
14 ML_file \<open>Tools/Function/function_context_tree.ML\<close> |
15 |
15 |
16 attribute_setup fundef_cong = |
16 attribute_setup fundef_cong = |
17 \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close> |
17 \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close> |
18 "declaration of congruence rule for function definitions" |
18 "declaration of congruence rule for function definitions" |
19 |
19 |
20 ML_file "Tools/Function/sum_tree.ML" |
20 ML_file \<open>Tools/Function/sum_tree.ML\<close> |
21 |
21 |
22 end |
22 end |