1 theory My_block

     2 imports Main

     3 keywords 

     4   "my_block" :: prf_script and 

     5   "my_block_end" :: prf_script and 

     6   "my_note" :: prf_decl

     7 begin

     8 

     9 ML {*

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

    11 *}

    12 

    13 ML {*

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

    15 *}

    16 

    17 ML {*

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

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

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

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

    22 *}

    23 

    24 ML {*

    25   fun my_note x = 

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

    27 *}

    28 

    29 ML {*

    30 val _ =

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

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

    33 *}

    34 

    35 end

    36