--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Prove.thy	Mon Dec 07 14:09:50 2009 +0100
@@ -0,0 +1,28 @@
+theory Prove
+imports Plain 
+begin
+
+ML {*
+val r = Unsynchronized.ref (NONE:(unit -> term) option)
+*}
+
+ML {*
+let
+  fun after_qed thm_name thms lthy =
+       Local_Theory.note (thm_name, (flat thms)) lthy |> snd
+    
+  fun setup_proof (name_spec, (txt, pos)) lthy =
+  let
+    val trm = ML_Context.evaluate lthy true ("r", r) txt
+  in
+    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
+  end
+
+  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+in
+  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
+    OuterKeyword.thy_goal (parser >> setup_proof)
+end
+*}
+
+end