equal
deleted
inserted
replaced
18 |
18 |
19 use_thy "Pure"; |
19 use_thy "Pure"; |
20 structure Pure = struct val thy = theory "Pure" end; |
20 structure Pure = struct val thy = theory "Pure" end; |
21 |
21 |
22 Context.add_setup |
22 Context.add_setup |
23 (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
23 (Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #> |
24 Sign.add_syntax Syntax.applC_syntax); |
24 Sign.add_syntax_i PureThy.applC_syntax); |
25 use_thy "CPure"; |
25 use_thy "CPure"; |
26 structure CPure = struct val thy = theory "CPure" end; |
26 structure CPure = struct val thy = theory "CPure" end; |
27 |
27 |
28 |
28 |
29 (* ML toplevel pretty printing *) |
29 (* ML toplevel pretty printing *) |