author | wenzelm |
Wed, 05 May 1999 18:48:32 +0200 | |
changeset 6604 | d646567156c3 |
parent 6366 | 0be3281aa578 |
child 6653 | b0b819902eaa |
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 @ |
|
6313 | 12 |
HTML.setup @ |
5839 | 13 |
ProofContext.setup @ |
14 |
Method.setup @ |
|
6366 | 15 |
Attrib.setup @ |
16 |
AxClass.setup; |
|
5839 | 17 |
in |
18 |
structure Pure = |
|
19 |
struct |
|
20 |
val thy = |
|
21 |
PureThy.begin_theory "Pure" [ProtoPure.thy] |
|
22 |
|> Theory.add_syntax Syntax.pure_appl_syntax |
|
5905 | 23 |
|> Library.apply common_setup |
5839 | 24 |
|> PureThy.end_theory; |
25 |
end; |
|
5092 | 26 |
|
5839 | 27 |
structure CPure = |
28 |
struct |
|
29 |
val thy = |
|
30 |
PureThy.begin_theory "CPure" [ProtoPure.thy] |
|
31 |
|> Theory.add_syntax Syntax.pure_applC_syntax |
|
5905 | 32 |
|> Library.apply common_setup |
5863 | 33 |
|> Theory.copy |
5839 | 34 |
|> PureThy.end_theory; |
35 |
end; |
|
5211 | 36 |
end; |
5092 | 37 |
|
6192
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
38 |
ThyInfo.register_theory ProtoPure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
39 |
ThyInfo.register_theory Pure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
40 |
ThyInfo.register_theory CPure.thy; |