thys/My_block.thy
changeset 9 b88fc9da1970
parent 0 1378b654acde
--- a/thys/My_block.thy	Mon Mar 24 11:39:39 2014 +0000
+++ b/thys/My_block.thy	Mon Mar 24 12:15:55 2014 +0000
@@ -7,11 +7,16 @@
 begin
 
 ML {*
-  val my_block = Proof.assert_backward #> Proof.enter_forward #> Proof.begin_block
+  val my_block = 
+    Proof.assert_backward 
+    #> Proof.enter_forward 
+    #> Proof.begin_block
 *}
 
 ML {*
-  val my_block_end = Proof.end_block #> Proof.enter_backward
+  val my_block_end = 
+    Proof.end_block 
+    #> Proof.enter_backward
 *}
 
 ML {*
@@ -23,7 +28,10 @@
 
 ML {*
   fun my_note x = 
-     Proof.assert_backward #> Proof.enter_forward #> Proof.note_thmss_cmd x #> Proof.enter_backward
+    Proof.assert_backward 
+    #> Proof.enter_forward 
+    #> Proof.note_thmss_cmd x 
+    #> Proof.enter_backward
 *}
 
 ML {*