equal
deleted
inserted
replaced
99 |
99 |
100 use_thy "Pure"; |
100 use_thy "Pure"; |
101 structure Pure = struct val thy = theory "Pure" end; |
101 structure Pure = struct val thy = theory "Pure" end; |
102 |
102 |
103 Context.add_setup |
103 Context.add_setup |
104 (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
104 (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> |
105 Theory.add_syntax Syntax.applC_syntax); |
105 Sign.add_syntax Syntax.applC_syntax); |
106 use_thy "CPure"; |
106 use_thy "CPure"; |
107 structure CPure = struct val thy = theory "CPure" end; |
107 structure CPure = struct val thy = theory "CPure" end; |
108 |
108 |
109 (*final ML setup*) |
109 (*final ML setup*) |
110 use "install_pp.ML"; |
110 use "install_pp.ML"; |