equal
deleted
inserted
replaced
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 "Tools/Function/function_lib.ML" |
|
12 named_theorems termination_simp "simplification rules for termination proofs" |
12 ML_file "Tools/Function/function_common.ML" |
13 ML_file "Tools/Function/function_common.ML" |
13 ML_file "Tools/Function/context_tree.ML" |
14 ML_file "Tools/Function/context_tree.ML" |
14 setup Function_Ctx_Tree.setup |
15 setup Function_Ctx_Tree.setup |
15 ML_file "Tools/Function/sum_tree.ML" |
16 ML_file "Tools/Function/sum_tree.ML" |
16 |
17 |