author | wenzelm |
Sun, 29 Jan 2006 19:23:44 +0100 | |
changeset 18837 | 577438cc653e |
parent 18836 | 3a1e4ee72075 |
child 18838 | d32f70789342 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Sun Jan 29 19:23:43 2006 +0100 +++ b/src/Pure/ROOT.ML Sun Jan 29 19:23:44 2006 +0100 @@ -90,6 +90,10 @@ setmp proofs 1 use "proof_general.ML"; use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end; + +Context.add_setup + (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> + Theory.add_syntax Syntax.applC_syntax); use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end; (*final ML setup*)