--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Prove.thy	Tue Aug 25 00:30:23 2009 +0200
@@ -0,0 +1,26 @@
+theory Prove
+imports Main
+begin
+
+ML {*
+val r = ref (NONE:(unit -> term) option)
+*}
+ML {*
+let
+   fun setup_proof (txt, pos) lthy =
+   let
+     val trm = ML_Context.evaluate lthy true ("r", r) txt
+   in
+       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
+   end;
+
+   val setup_proof_parser = OuterParse.ML_source >> setup_proof
+        
+   val kind = OuterKeyword.thy_goal
+in
+   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
+    kind setup_proof_parser
+end
+*}
+
+end