equal
deleted
inserted
replaced
1 theory Command |
1 theory Command |
2 imports Main |
2 imports Main |
|
3 keywords "foobar" "foobar_trace" :: thy_decl and |
|
4 "foobar_goal" "foobar_prove" :: thy_goal |
3 begin |
5 begin |
4 |
6 |
5 ML {* |
7 ML {* |
6 let |
8 let |
7 val do_nothing = Scan.succeed (Local_Theory.background_theory I) |
9 val do_nothing = Scan.succeed (Local_Theory.background_theory I) |
8 val kind = Keyword.thy_decl |
10 val kind = Keyword.thy_decl |
9 in |
11 in |
10 Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing |
12 Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing |
11 end |
13 end |
12 *} |
14 *} |
13 |
15 |
14 ML {* |
16 ML {* |
15 let |
17 let |
16 fun trace_prop str = |
18 fun trace_prop str = |
17 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
19 Local_Theory.background_theory (fn lthy => (tracing str; lthy)) |
18 val trace_prop_parser = Parse.prop >> trace_prop |
20 val trace_prop_parser = Parse.prop >> trace_prop |
19 val kind = Keyword.thy_decl |
21 val kind = Keyword.thy_decl |
20 in |
22 in |
21 Outer_Syntax.local_theory "foobar_trace" "traces a proposition" |
23 Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" |
22 kind trace_prop_parser |
24 trace_prop_parser |
23 end |
25 end |
24 *} |
26 *} |
25 |
27 |
26 ML {* |
28 ML {* |
27 let |
29 let |
32 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
34 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
33 end; |
35 end; |
34 val prove_prop_parser = Parse.prop >> prove_prop |
36 val prove_prop_parser = Parse.prop >> prove_prop |
35 val kind = Keyword.thy_goal |
37 val kind = Keyword.thy_goal |
36 in |
38 in |
37 Outer_Syntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
39 Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proving a proposition" |
38 kind prove_prop_parser |
40 prove_prop_parser |
39 end |
41 end |
40 *} |
42 *} |
41 |
43 |
42 ML {* |
44 ML {* |
43 structure Result = Proof_Data( |
45 structure Result = Proof_Data( |
60 end |
62 end |
61 |
63 |
62 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
64 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
63 |
65 |
64 in |
66 in |
65 Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
67 Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) "proving a proposition" |
66 Keyword.thy_goal (parser >> setup_proof) |
68 (parser >> setup_proof) |
67 end*} |
69 end*} |
68 |
70 |
69 |
71 |
70 |
72 |
71 |
73 |