equal
deleted
inserted
replaced
2 imports Main |
2 imports Main |
3 keywords "foobar" "foobar_trace" :: thy_decl and |
3 keywords "foobar" "foobar_trace" :: thy_decl and |
4 "foobar_goal" "foobar_prove" :: thy_goal |
4 "foobar_goal" "foobar_prove" :: thy_goal |
5 begin |
5 begin |
6 |
6 |
7 ML {* |
7 ML \<open> |
8 let |
8 let |
9 val do_nothing = Scan.succeed (Local_Theory.background_theory I) |
9 val do_nothing = Scan.succeed (Local_Theory.background_theory I) |
10 in |
10 in |
11 Outer_Syntax.local_theory @{command_spec "foobar"} |
11 Outer_Syntax.local_theory @{command_spec "foobar"} |
12 "description of foobar" |
12 "description of foobar" |
13 do_nothing |
13 do_nothing |
14 end |
14 end |
15 *} |
15 \<close> |
16 |
16 |
17 ML {* |
17 ML \<open> |
18 let |
18 let |
19 fun trace_prop str = |
19 fun trace_prop str = |
20 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
20 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
21 val trace_prop_parser = Parse.prop >> trace_prop |
21 val trace_prop_parser = Parse.prop >> trace_prop |
22 in |
22 in |
23 Outer_Syntax.local_theory @{command_spec "foobar_trace"} |
23 Outer_Syntax.local_theory @{command_spec "foobar_trace"} |
24 "traces a proposition" |
24 "traces a proposition" |
25 trace_prop_parser |
25 trace_prop_parser |
26 end |
26 end |
27 *} |
27 \<close> |
28 |
28 |
29 ML {* |
29 ML \<open> |
30 let |
30 let |
31 fun prove_prop str lthy = |
31 fun prove_prop str lthy = |
32 let |
32 let |
33 val prop = Syntax.read_prop lthy str |
33 val prop = Syntax.read_prop lthy str |
34 in |
34 in |
38 in |
38 in |
39 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} |
39 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} |
40 "proving a proposition" |
40 "proving a proposition" |
41 prove_prop_parser |
41 prove_prop_parser |
42 end |
42 end |
43 *} |
43 \<close> |
44 |
44 |
45 ML {* |
45 ML \<open> |
46 structure Result = Proof_Data( |
46 structure Result = Proof_Data( |
47 type T = unit -> term |
47 type T = unit -> term |
48 fun init thy () = error "Result") |
48 fun init thy () = error "Result") |
49 |
49 |
50 val result_cookie = (Result.get, Result.put, "Result.put") |
50 val result_cookie = (Result.get, Result.put, "Result.put") |
51 *} |
51 \<close> |
52 |
52 |
53 ML{* |
53 ML\<open> |
54 let |
54 let |
55 fun after_qed thm_name thms lthy = |
55 fun after_qed thm_name thms lthy = |
56 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
56 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
57 |
57 |
58 fun setup_proof (thm_name, {text, ...}) lthy = |
58 fun setup_proof (thm_name, {text, ...}) lthy = |
66 |
66 |
67 in |
67 in |
68 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} |
68 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} |
69 "proving a proposition" |
69 "proving a proposition" |
70 (parser >> setup_proof) |
70 (parser >> setup_proof) |
71 end*} |
71 end\<close> |
72 |
72 |
73 |
73 |
74 |
74 |
75 |
75 |
76 end |
76 end |