equal
deleted
inserted
replaced
5 "my_block_end" :: prf_script and |
5 "my_block_end" :: prf_script and |
6 "my_note" :: prf_decl |
6 "my_note" :: prf_decl |
7 begin |
7 begin |
8 |
8 |
9 ML {* |
9 ML {* |
10 val my_block = Proof.assert_backward #> Proof.enter_forward #> Proof.begin_block |
10 val my_block = |
|
11 Proof.assert_backward |
|
12 #> Proof.enter_forward |
|
13 #> Proof.begin_block |
11 *} |
14 *} |
12 |
15 |
13 ML {* |
16 ML {* |
14 val my_block_end = Proof.end_block #> Proof.enter_backward |
17 val my_block_end = |
|
18 Proof.end_block |
|
19 #> Proof.enter_backward |
15 *} |
20 *} |
16 |
21 |
17 ML {* |
22 ML {* |
18 val _ = Outer_Syntax.command @{command_spec "my_block"} "begin my block" |
23 val _ = Outer_Syntax.command @{command_spec "my_block"} "begin my block" |
19 (Scan.succeed (Toplevel.print o (Toplevel.proof my_block))) |
24 (Scan.succeed (Toplevel.print o (Toplevel.proof my_block))) |
21 (Scan.succeed (Toplevel.print o (Toplevel.proof my_block_end))) |
26 (Scan.succeed (Toplevel.print o (Toplevel.proof my_block_end))) |
22 *} |
27 *} |
23 |
28 |
24 ML {* |
29 ML {* |
25 fun my_note x = |
30 fun my_note x = |
26 Proof.assert_backward #> Proof.enter_forward #> Proof.note_thmss_cmd x #> Proof.enter_backward |
31 Proof.assert_backward |
|
32 #> Proof.enter_forward |
|
33 #> Proof.note_thmss_cmd x |
|
34 #> Proof.enter_backward |
27 *} |
35 *} |
28 |
36 |
29 ML {* |
37 ML {* |
30 val _ = |
38 val _ = |
31 Outer_Syntax.command @{command_spec "my_note"} "define facts" |
39 Outer_Syntax.command @{command_spec "my_note"} "define facts" |