| author | berghofe |
| Wed Oct 31 19:37:04 2001 +0100 (2001-10-31) | |
| changeset 11998 | b14e7686ce84 |
| parent 11761 | 183435fd45f2 |
| child 12013 | 8d2372c6b5f3 |
| permissions | -rw-r--r-- |
| wenzelm@5092 | 1 |
(* Title: Pure/pure.ML |
| wenzelm@5092 | 2 |
ID: $Id$ |
| wenzelm@5092 | 3 |
Author: Markus Wenzel, TU Muenchen |
| wenzelm@5092 | 4 |
|
| wenzelm@6192 | 5 |
Final setup of the Pure theories. |
| wenzelm@5092 | 6 |
*) |
| wenzelm@5092 | 7 |
|
| wenzelm@5839 | 8 |
local |
| wenzelm@5839 | 9 |
val common_setup = |
| wenzelm@5839 | 10 |
Locale.setup @ |
| wenzelm@6313 | 11 |
HTML.setup @ |
| wenzelm@11761 | 12 |
ObjectLogic.setup @ |
| wenzelm@5839 | 13 |
ProofContext.setup @ |
| wenzelm@6770 | 14 |
Attrib.setup @ |
| wenzelm@11664 | 15 |
InductAttrib.setup @ |
| wenzelm@5839 | 16 |
Method.setup @ |
| wenzelm@6770 | 17 |
Calculation.setup @ |
| wenzelm@6888 | 18 |
SkipProof.setup @ |
| berghofe@6653 | 19 |
AxClass.setup @ |
| wenzelm@8965 | 20 |
Latex.setup @ |
| wenzelm@7718 | 21 |
Present.setup @ |
| wenzelm@6696 | 22 |
Isamode.setup @ |
| berghofe@11515 | 23 |
ProofGeneral.setup @ |
| berghofe@11515 | 24 |
Codegen.setup; |
| wenzelm@5839 | 25 |
in |
| wenzelm@5839 | 26 |
structure Pure = |
| wenzelm@5839 | 27 |
struct |
| wenzelm@5839 | 28 |
val thy = |
| wenzelm@10931 | 29 |
PureThy.begin_theory Sign.PureN [ProtoPure.thy] |
| wenzelm@5839 | 30 |
|> Theory.add_syntax Syntax.pure_appl_syntax |
| wenzelm@5905 | 31 |
|> Library.apply common_setup |
| wenzelm@5839 | 32 |
|> PureThy.end_theory; |
| wenzelm@5839 | 33 |
end; |
| wenzelm@5092 | 34 |
|
| wenzelm@5839 | 35 |
structure CPure = |
| wenzelm@5839 | 36 |
struct |
| wenzelm@5839 | 37 |
val thy = |
| wenzelm@10931 | 38 |
PureThy.begin_theory Sign.CPureN [ProtoPure.thy] |
| wenzelm@5839 | 39 |
|> Theory.add_syntax Syntax.pure_applC_syntax |
| wenzelm@5905 | 40 |
|> Library.apply common_setup |
| wenzelm@5863 | 41 |
|> Theory.copy |
| wenzelm@5839 | 42 |
|> PureThy.end_theory; |
| wenzelm@5839 | 43 |
end; |
| wenzelm@5211 | 44 |
end; |
| wenzelm@5092 | 45 |
|
| wenzelm@6192 | 46 |
ThyInfo.register_theory ProtoPure.thy; |
| wenzelm@6192 | 47 |
ThyInfo.register_theory Pure.thy; |
| wenzelm@6192 | 48 |
ThyInfo.register_theory CPure.thy; |