# HG changeset patch
# User wenzelm
# Date 1184671187 -7200
# Node ID a8a3962f8eebd87c9dbd2b2715ef3e9f129b1214
# Parent  0f0d1cf4992d4ca398a008138de0bdb32b28f016
Pure theory setup.

diff -r 0f0d1cf4992d -r a8a3962f8eeb 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;