--- 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 {*