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