equal
deleted
inserted
replaced
16 ("Tools/function_package/sum_tree.ML") |
16 ("Tools/function_package/sum_tree.ML") |
17 ("Tools/function_package/mutual.ML") |
17 ("Tools/function_package/mutual.ML") |
18 ("Tools/function_package/pattern_split.ML") |
18 ("Tools/function_package/pattern_split.ML") |
19 ("Tools/function_package/fundef_package.ML") |
19 ("Tools/function_package/fundef_package.ML") |
20 ("Tools/function_package/auto_term.ML") |
20 ("Tools/function_package/auto_term.ML") |
21 ("Tools/function_package/induction_scheme.ML") |
|
22 ("Tools/function_package/measure_functions.ML") |
21 ("Tools/function_package/measure_functions.ML") |
23 ("Tools/function_package/lexicographic_order.ML") |
22 ("Tools/function_package/lexicographic_order.ML") |
24 ("Tools/function_package/fundef_datatype.ML") |
23 ("Tools/function_package/fundef_datatype.ML") |
|
24 ("Tools/function_package/induction_scheme.ML") |
25 begin |
25 begin |
26 |
26 |
27 text {* Definitions with default value. *} |
27 text {* Definitions with default value. *} |
28 |
28 |
29 definition |
29 definition |
108 use "Tools/function_package/sum_tree.ML" |
108 use "Tools/function_package/sum_tree.ML" |
109 use "Tools/function_package/mutual.ML" |
109 use "Tools/function_package/mutual.ML" |
110 use "Tools/function_package/pattern_split.ML" |
110 use "Tools/function_package/pattern_split.ML" |
111 use "Tools/function_package/auto_term.ML" |
111 use "Tools/function_package/auto_term.ML" |
112 use "Tools/function_package/fundef_package.ML" |
112 use "Tools/function_package/fundef_package.ML" |
113 use "Tools/function_package/induction_scheme.ML" |
|
114 use "Tools/function_package/measure_functions.ML" |
113 use "Tools/function_package/measure_functions.ML" |
115 use "Tools/function_package/lexicographic_order.ML" |
114 use "Tools/function_package/lexicographic_order.ML" |
116 use "Tools/function_package/fundef_datatype.ML" |
115 use "Tools/function_package/fundef_datatype.ML" |
|
116 use "Tools/function_package/induction_scheme.ML" |
117 |
117 |
118 setup {* |
118 setup {* |
119 FundefPackage.setup |
119 FundefPackage.setup |
120 #> InductionScheme.setup |
120 #> InductionScheme.setup |
121 #> MeasureFunctions.setup |
121 #> MeasureFunctions.setup |