1 theory My_block

     2 imports Main

     3 keywords "my_block" :: prf_script and "my_block_end" :: prf_script  

     4   and "my_note" :: prf_decl

     5 begin

     6 

     7 ML {*

     8   val my_block = Proof.assert_backward #> Proof.enter_forward #> Proof.begin_block

     9 *}

    10 

    11 ML {*

    12   val my_block_end = Proof.end_block #> Proof.enter_backward

    13 *}

    14 

    15 ML {*

    16   val _ = Outer_Syntax.command @{command_spec "my_block"} "begin my block"

    17         (Scan.succeed (Toplevel.print o (Toplevel.proof my_block)))

    18   val _ = Outer_Syntax.command @{command_spec "my_block_end"} "begin my block"

    19         (Scan.succeed (Toplevel.print o (Toplevel.proof my_block_end)))

    20 *}

    21 

    22 ML {*

    23   fun my_note x = 

    24      Proof.assert_backward #> Proof.enter_forward #> Proof.note_thmss_cmd x #> Proof.enter_backward

    25 *}

    26 

    27 ML {*

    28 val _ =

    29   Outer_Syntax.command @{command_spec "my_note"} "define facts"

    30     (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o my_note)));

    31 *}

    32 

    33 end

    34