| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Mon, 24 Mar 2014 12:15:55 +0000 | |
| changeset 9 | b88fc9da1970 |
| parent 0 | 1378b654acde |
| permissions | -rw-r--r-- |
|
0
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory My_block |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports Main |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
keywords |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
"my_block" :: prf_script and |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
"my_block_end" :: prf_script and |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
"my_note" :: prf_decl |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
begin |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
ML {*
|
|
9
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
10 |
val my_block = |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
11 |
Proof.assert_backward |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
12 |
#> Proof.enter_forward |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
13 |
#> Proof.begin_block |
|
0
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
ML {*
|
|
9
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
17 |
val my_block_end = |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
18 |
Proof.end_block |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
19 |
#> Proof.enter_backward |
|
0
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
ML {*
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
val _ = Outer_Syntax.command @{command_spec "my_block"} "begin my block"
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
(Scan.succeed (Toplevel.print o (Toplevel.proof my_block))) |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
val _ = Outer_Syntax.command @{command_spec "my_block_end"} "begin my block"
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
(Scan.succeed (Toplevel.print o (Toplevel.proof my_block_end))) |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
ML {*
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
fun my_note x = |
|
9
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
31 |
Proof.assert_backward |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
32 |
#> Proof.enter_forward |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
33 |
#> Proof.note_thmss_cmd x |
|
b88fc9da1970
small modifications
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
34 |
#> Proof.enter_backward |
|
0
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
ML {*
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
val _ = |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
Outer_Syntax.command @{command_spec "my_note"} "define facts"
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
(Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o my_note))); |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
end |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |