equal
deleted
inserted
replaced
6 header {* General recursive function definitions *} |
6 header {* General recursive function definitions *} |
7 |
7 |
8 theory FunDef |
8 theory FunDef |
9 imports Datatype Accessible_Part |
9 imports Datatype Accessible_Part |
10 uses |
10 uses |
11 ("Tools/function_package/sum_tools.ML") |
|
12 ("Tools/function_package/fundef_lib.ML") |
11 ("Tools/function_package/fundef_lib.ML") |
13 ("Tools/function_package/fundef_common.ML") |
12 ("Tools/function_package/fundef_common.ML") |
14 ("Tools/function_package/inductive_wrap.ML") |
13 ("Tools/function_package/inductive_wrap.ML") |
15 ("Tools/function_package/context_tree.ML") |
14 ("Tools/function_package/context_tree.ML") |
16 ("Tools/function_package/fundef_core.ML") |
15 ("Tools/function_package/fundef_core.ML") |
84 thus ?thesis |
83 thus ?thesis |
85 unfolding f_def |
84 unfolding f_def |
86 by (rule THE_default_none) |
85 by (rule THE_default_none) |
87 qed |
86 qed |
88 |
87 |
89 |
|
90 use "Tools/function_package/sum_tools.ML" |
|
91 use "Tools/function_package/fundef_lib.ML" |
88 use "Tools/function_package/fundef_lib.ML" |
92 use "Tools/function_package/fundef_common.ML" |
89 use "Tools/function_package/fundef_common.ML" |
93 use "Tools/function_package/inductive_wrap.ML" |
90 use "Tools/function_package/inductive_wrap.ML" |
94 use "Tools/function_package/context_tree.ML" |
91 use "Tools/function_package/context_tree.ML" |
95 use "Tools/function_package/fundef_core.ML" |
92 use "Tools/function_package/fundef_core.ML" |