equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
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 Option Accessible_Part |
10 uses |
10 uses |
11 ("Tools/function_package/fundef_lib.ML") |
11 ("Tools/function_package/fundef_lib.ML") |
12 ("Tools/function_package/fundef_common.ML") |
12 ("Tools/function_package/fundef_common.ML") |
13 ("Tools/function_package/inductive_wrap.ML") |
13 ("Tools/function_package/inductive_wrap.ML") |
14 ("Tools/function_package/context_tree.ML") |
14 ("Tools/function_package/context_tree.ML") |