--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/My_block.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,34 @@
+theory My_block
+imports Main
+keywords "my_block" :: prf_script and "my_block_end" :: prf_script  
+  and "my_note" :: prf_decl
+begin
+
+ML {*
+  val my_block = Proof.assert_backward #> Proof.enter_forward #> Proof.begin_block
+*}
+
+ML {*
+  val my_block_end = Proof.end_block #> Proof.enter_backward
+*}
+
+ML {*
+  val _ = Outer_Syntax.command @{command_spec "my_block"} "begin my block"
+        (Scan.succeed (Toplevel.print o (Toplevel.proof my_block)))
+  val _ = Outer_Syntax.command @{command_spec "my_block_end"} "begin my block"
+        (Scan.succeed (Toplevel.print o (Toplevel.proof my_block_end)))
+*}
+
+ML {*
+  fun my_note x = 
+     Proof.assert_backward #> Proof.enter_forward #> Proof.note_thmss_cmd x #> Proof.enter_backward
+*}
+
+ML {*
+val _ =
+  Outer_Syntax.command @{command_spec "my_note"} "define facts"
+    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o my_note)));
+*}
+
+end
+