diff -r dcbf7888a070 -r b88fc9da1970 thys/My_block.thy --- 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 {*