7701
|
1 |
(* Title: HOL/Recdef.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Konrad Slind
|
5123
|
4 |
|
7701
|
5 |
TFL: recursive function definitions.
|
|
6 |
*)
|
|
7 |
|
|
8 |
theory Recdef = WF_Rel + Datatype
|
|
9 |
files
|
|
10 |
(*establish a base of common and/or helpful functions*)
|
|
11 |
"../TFL/utils.sig"
|
|
12 |
|
|
13 |
"../TFL/usyntax.sig"
|
|
14 |
"../TFL/rules.sig"
|
|
15 |
"../TFL/thry.sig"
|
|
16 |
"../TFL/thms.sig"
|
|
17 |
"../TFL/tfl.sig"
|
|
18 |
"../TFL/utils.sml"
|
|
19 |
|
|
20 |
(*supply implementations*)
|
|
21 |
"../TFL/usyntax.sml"
|
|
22 |
"../TFL/thms.sml"
|
|
23 |
"../TFL/dcterm.sml"
|
|
24 |
"../TFL/rules.sml"
|
|
25 |
"../TFL/thry.sml"
|
|
26 |
|
|
27 |
(*link system and specialize for Isabelle*)
|
|
28 |
"../TFL/tfl.sml"
|
|
29 |
"../TFL/post.sml"
|
|
30 |
|
|
31 |
(*theory extender wrapper module*)
|
8303
|
32 |
"Tools/recdef_package.ML":
|
6438
|
33 |
|
|
34 |
setup RecdefPackage.setup
|
|
35 |
|
|
36 |
end
|