author | wenzelm |
Tue, 02 Jul 2002 15:36:51 +0200 | |
changeset 13271 | d0859ff6cd65 |
parent 12723 | 0451211bf4a0 |
child 13402 | e6e826bb8c3c |
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 = |
|
12234 | 10 |
ProofRewriteRules.setup @ |
6313 | 11 |
HTML.setup @ |
11761 | 12 |
ObjectLogic.setup @ |
5839 | 13 |
ProofContext.setup @ |
12234 | 14 |
Locale.setup @ |
6770 | 15 |
Attrib.setup @ |
12350 | 16 |
ContextRules.setup @ |
11664 | 17 |
InductAttrib.setup @ |
5839 | 18 |
Method.setup @ |
6770 | 19 |
Calculation.setup @ |
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6785
diff
changeset
|
20 |
SkipProof.setup @ |
6653 | 21 |
AxClass.setup @ |
8965 | 22 |
Latex.setup @ |
7718 | 23 |
Present.setup @ |
11515 | 24 |
ProofGeneral.setup @ |
12013 | 25 |
Codegen.setup @ |
26 |
Goals.setup; |
|
5839 | 27 |
in |
28 |
structure Pure = |
|
29 |
struct |
|
30 |
val thy = |
|
10931 | 31 |
PureThy.begin_theory Sign.PureN [ProtoPure.thy] |
5839 | 32 |
|> Theory.add_syntax Syntax.pure_appl_syntax |
5905 | 33 |
|> Library.apply common_setup |
5839 | 34 |
|> PureThy.end_theory; |
35 |
end; |
|
5092 | 36 |
|
5839 | 37 |
structure CPure = |
38 |
struct |
|
39 |
val thy = |
|
10931 | 40 |
PureThy.begin_theory Sign.CPureN [ProtoPure.thy] |
5839 | 41 |
|> Theory.add_syntax Syntax.pure_applC_syntax |
5905 | 42 |
|> Library.apply common_setup |
5863 | 43 |
|> Theory.copy |
5839 | 44 |
|> PureThy.end_theory; |
45 |
end; |
|
5211 | 46 |
end; |
5092 | 47 |
|
6192
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
48 |
ThyInfo.register_theory ProtoPure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
49 |
ThyInfo.register_theory Pure.thy; |
a42dbf1af868
proper setup of preloaded theories (ThyInfo.register_theory);
wenzelm
parents:
5905
diff
changeset
|
50 |
ThyInfo.register_theory CPure.thy; |