5092
|
1 |
(* Title: Pure/pure.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
5211
|
5 |
Setup the actual Pure and CPure 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
|
|
21 |
|> Theory.apply common_setup
|
|
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
|
|
30 |
|> Theory.apply common_setup
|
5863
|
31 |
|> Theory.copy
|
5839
|
32 |
|> PureThy.end_theory;
|
|
33 |
end;
|
5211
|
34 |
end;
|
5092
|
35 |
|
5211
|
36 |
ThyInfo.loaded_thys :=
|
|
37 |
(Symtab.make (map ThyInfo.mk_info
|
|
38 |
[("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
|
|
39 |
("Pure", [], ["ProtoPure"], Pure.thy),
|
|
40 |
("CPure", [], ["ProtoPure"], CPure.thy)]));
|