equal
deleted
inserted
replaced
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 |
10 val kind = Keyword.thy_decl |
11 in |
11 in |
12 Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing |
12 Outer_Syntax.local_theory @{command_spec "foobar"} |
|
13 "description of foobar" |
|
14 do_nothing |
13 end |
15 end |
14 *} |
16 *} |
15 |
17 |
16 ML {* |
18 ML {* |
17 let |
19 let |
18 fun trace_prop str = |
20 fun trace_prop str = |
19 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
21 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
20 val trace_prop_parser = Parse.prop >> trace_prop |
22 val trace_prop_parser = Parse.prop >> trace_prop |
21 val kind = Keyword.thy_decl |
23 val kind = Keyword.thy_decl |
22 in |
24 in |
23 Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" |
25 Outer_Syntax.local_theory @{command_spec "foobar_trace"} |
24 trace_prop_parser |
26 "traces a proposition" |
|
27 trace_prop_parser |
25 end |
28 end |
26 *} |
29 *} |
27 |
30 |
28 ML {* |
31 ML {* |
29 let |
32 let |
34 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
37 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
35 end; |
38 end; |
36 val prove_prop_parser = Parse.prop >> prove_prop |
39 val prove_prop_parser = Parse.prop >> prove_prop |
37 val kind = Keyword.thy_goal |
40 val kind = Keyword.thy_goal |
38 in |
41 in |
39 Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proving a proposition" |
42 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} |
40 prove_prop_parser |
43 "proving a proposition" |
|
44 prove_prop_parser |
41 end |
45 end |
42 *} |
46 *} |
43 |
47 |
44 ML {* |
48 ML {* |
45 structure Result = Proof_Data( |
49 structure Result = Proof_Data( |
62 end |
66 end |
63 |
67 |
64 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
68 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
65 |
69 |
66 in |
70 in |
67 Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) "proving a proposition" |
71 Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} |
68 (parser >> setup_proof) |
72 "proving a proposition" |
|
73 (parser >> setup_proof) |
69 end*} |
74 end*} |
70 |
75 |
71 |
76 |
72 |
77 |
73 |
78 |