--- a/ProgTutorial/Helper/Command/Command.thy	Fri Aug 21 16:23:51 2009 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Sat Aug 22 02:56:08 2009 +0200
@@ -1,10 +1,11 @@
 theory Command
 imports Main
 begin
+
 ML {*
 let
    val do_nothing = Scan.succeed (LocalTheory.theory I)
-   val kind = OuterKeyword.thy_goal
+   val kind = OuterKeyword.thy_decl
 in
    OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
 end
@@ -12,11 +13,61 @@
 
 ML {*
 let
+  fun trace_prop str =
+     LocalTheory.theory (fn lthy => (tracing str; lthy))
+  val trace_prop_parser = OuterParse.prop >> trace_prop
+  val kind = OuterKeyword.thy_decl
+in
+  OuterSyntax.local_theory "foobar_trace" "traces a proposition"
+    kind trace_prop_parser
+end
+*}
+
+ML {*
+let
+   fun prove_prop str lthy =
+     let
+       val prop = Syntax.read_prop lthy str
+     in
+       Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
+     end;
+   val prove_prop_parser = OuterParse.prop >> prove_prop
+   val kind = OuterKeyword.thy_goal
+in
+   OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition"
+     kind prove_prop_parser
+end
+*}
+
+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 "foobar_prove" "proving a proposition" 
+    kind setup_proof_parser
+end
+*}
+
+(*
+ML {*
+let
    val do_nothing = Scan.succeed (LocalTheory.theory I)
    val kind = OuterKeyword.thy_decl
 in
-   OuterSyntax.local_theory "simple_induct" "description of foobar" kind do_nothing
+   OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing
 end
-*}
+*}*)
 
 end