equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 val r = ref (NONE:(unit -> term) option) |
6 val r = ref (NONE:(unit -> term) option) |
7 *} |
7 *} |
|
8 |
8 ML {* |
9 ML {* |
9 let |
10 let |
10 fun setup_proof (txt, pos) lthy = |
11 fun setup_proof (txt, pos) lthy = |
11 let |
12 let |
12 val trm = ML_Context.evaluate lthy true ("r", r) txt |
13 val trm = ML_Context.evaluate lthy true ("r", r) txt |
16 |
17 |
17 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
18 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
18 |
19 |
19 val kind = OuterKeyword.thy_goal |
20 val kind = OuterKeyword.thy_goal |
20 in |
21 in |
21 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
22 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
22 kind setup_proof_parser |
23 kind setup_proof_parser |
23 end |
24 end |
24 *} |
25 *} |
25 |
26 |
|
27 |
|
28 |
26 end |
29 end |