author | wenzelm |
Wed, 03 Feb 1999 16:47:37 +0100 | |
changeset 6192 | a42dbf1af868 |
parent 5905 | 68cdba6c178f |
child 6313 | 6e4c7209ff39 |
permissions | -rw-r--r-- |
5092 | 1 |
(* Title: Pure/pure.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
6192
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
5 |
Final setup of the Pure theories. |
5092 | 6 |
*) |
7 |
||
5839 | 8 |
local |
9 |
val common_setup = |
|
10 |
ObjectLogic.setup @ |
|
11 |
Locale.setup @ |
|
12 |
ProofContext.setup @ |
|
13 |
Method.setup @ |
|
14 |
Attrib.setup; |
|
15 |
in |
|
16 |
structure Pure = |
|
17 |
struct |
|
18 |
val thy = |
|
19 |
PureThy.begin_theory "Pure" [ProtoPure.thy] |
|
20 |
|> Theory.add_syntax Syntax.pure_appl_syntax |
|
5905 | 21 |
|> Library.apply common_setup |
5839 | 22 |
|> PureThy.end_theory; |
23 |
end; |
|
5092 | 24 |
|
5839 | 25 |
structure CPure = |
26 |
struct |
|
27 |
val thy = |
|
28 |
PureThy.begin_theory "CPure" [ProtoPure.thy] |
|
29 |
|> Theory.add_syntax Syntax.pure_applC_syntax |
|
5905 | 30 |
|> Library.apply common_setup |
5863 | 31 |
|> Theory.copy |
5839 | 32 |
|> PureThy.end_theory; |
33 |
end; |
|
5211 | 34 |
end; |
5092 | 35 |
|
6192
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
36 |
ThyInfo.register_theory ProtoPure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
37 |
ThyInfo.register_theory Pure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
38 |
ThyInfo.register_theory CPure.thy; |