equal
deleted
inserted
replaced
5 begin |
5 begin |
6 |
6 |
7 ML {* |
7 ML {* |
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 val kind = Keyword.thy_decl |
|
11 in |
10 in |
12 Outer_Syntax.local_theory @{command_spec "foobar"} |
11 Outer_Syntax.local_theory @{command_spec "foobar"} |
13 "description of foobar" |
12 "description of foobar" |
14 do_nothing |
13 do_nothing |
15 end |
14 end |
18 ML {* |
17 ML {* |
19 let |
18 let |
20 fun trace_prop str = |
19 fun trace_prop str = |
21 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
20 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
22 val trace_prop_parser = Parse.prop >> trace_prop |
21 val trace_prop_parser = Parse.prop >> trace_prop |
23 val kind = Keyword.thy_decl |
|
24 in |
22 in |
25 Outer_Syntax.local_theory @{command_spec "foobar_trace"} |
23 Outer_Syntax.local_theory @{command_spec "foobar_trace"} |
26 "traces a proposition" |
24 "traces a proposition" |
27 trace_prop_parser |
25 trace_prop_parser |
28 end |
26 end |
35 val prop = Syntax.read_prop lthy str |
33 val prop = Syntax.read_prop lthy str |
36 in |
34 in |
37 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
35 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
38 end; |
36 end; |
39 val prove_prop_parser = Parse.prop >> prove_prop |
37 val prove_prop_parser = Parse.prop >> prove_prop |
40 val kind = Keyword.thy_goal |
|
41 in |
38 in |
42 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} |
39 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} |
43 "proving a proposition" |
40 "proving a proposition" |
44 prove_prop_parser |
41 prove_prop_parser |
45 end |
42 end |
56 ML{* |
53 ML{* |
57 let |
54 let |
58 fun after_qed thm_name thms lthy = |
55 fun after_qed thm_name thms lthy = |
59 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
56 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
60 |
57 |
61 fun setup_proof (thm_name, (txt, pos)) lthy = |
58 fun setup_proof (thm_name, {text, ...}) lthy = |
62 let |
59 let |
63 val trm = Code_Runtime.value lthy result_cookie ("", txt) |
60 val trm = Code_Runtime.value lthy result_cookie ("", text) |
64 in |
61 in |
65 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
62 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
66 end |
63 end |
67 |
64 |
68 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
65 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |