equal
deleted
inserted
replaced
16 structure Pure = |
16 structure Pure = |
17 struct |
17 struct |
18 val thy = |
18 val thy = |
19 PureThy.begin_theory "Pure" [ProtoPure.thy] |
19 PureThy.begin_theory "Pure" [ProtoPure.thy] |
20 |> Theory.add_syntax Syntax.pure_appl_syntax |
20 |> Theory.add_syntax Syntax.pure_appl_syntax |
21 |> Theory.apply common_setup |
21 |> Library.apply common_setup |
22 |> PureThy.end_theory; |
22 |> PureThy.end_theory; |
23 end; |
23 end; |
24 |
24 |
25 structure CPure = |
25 structure CPure = |
26 struct |
26 struct |
27 val thy = |
27 val thy = |
28 PureThy.begin_theory "CPure" [ProtoPure.thy] |
28 PureThy.begin_theory "CPure" [ProtoPure.thy] |
29 |> Theory.add_syntax Syntax.pure_applC_syntax |
29 |> Theory.add_syntax Syntax.pure_applC_syntax |
30 |> Theory.apply common_setup |
30 |> Library.apply common_setup |
31 |> Theory.copy |
31 |> Theory.copy |
32 |> PureThy.end_theory; |
32 |> PureThy.end_theory; |
33 end; |
33 end; |
34 end; |
34 end; |
35 |
35 |