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