Pure theory setup.
authorwenzelm
Tue, 17 Jul 2007 13:19:47 +0200
changeset 23828 a8a3962f8eeb
parent 23827 0f0d1cf4992d
child 23829 41014a878a7d
Pure theory setup.
src/Pure/pure_setup.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/pure_setup.ML	Tue Jul 17 13:19:47 2007 +0200
@@ -0,0 +1,22 @@
+(*  Title:      Pure/pure_setup.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Pure theory setup.
+*)
+
+use_thy "Pure";
+structure Pure = struct val thy = theory "Pure" end;
+
+Context.add_setup
+ (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
+  Sign.add_syntax Syntax.applC_syntax);
+use_thy "CPure";
+structure CPure = struct val thy = theory "CPure" end;
+
+use "install_pp.ML";
+val use = ThyInfo.use;
+val cd = File.cd o Path.explode;
+ml_prompts "ML> " "ML# ";
+
+proofs := 0;