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