equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 let |
6 let |
7 val do_nothing = Scan.succeed (Local_Theory.theory I) |
7 val do_nothing = Scan.succeed (Local_Theory.theory I) |
8 val kind = OuterKeyword.thy_decl |
8 val kind = Keyword.thy_decl |
9 in |
9 in |
10 OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing |
10 Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing |
11 end |
11 end |
12 *} |
12 *} |
13 |
13 |
14 ML {* |
14 ML {* |
15 let |
15 let |
16 fun trace_prop str = |
16 fun trace_prop str = |
17 Local_Theory.theory (fn lthy => (tracing str; lthy)) |
17 Local_Theory.theory (fn lthy => (tracing str; lthy)) |
18 val trace_prop_parser = OuterParse.prop >> trace_prop |
18 val trace_prop_parser = Parse.prop >> trace_prop |
19 val kind = OuterKeyword.thy_decl |
19 val kind = Keyword.thy_decl |
20 in |
20 in |
21 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
21 Outer_Syntax.local_theory "foobar_trace" "traces a proposition" |
22 kind trace_prop_parser |
22 kind trace_prop_parser |
23 end |
23 end |
24 *} |
24 *} |
25 |
25 |
26 ML {* |
26 ML {* |
29 let |
29 let |
30 val prop = Syntax.read_prop lthy str |
30 val prop = Syntax.read_prop lthy str |
31 in |
31 in |
32 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
32 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
33 end; |
33 end; |
34 val prove_prop_parser = OuterParse.prop >> prove_prop |
34 val prove_prop_parser = Parse.prop >> prove_prop |
35 val kind = OuterKeyword.thy_goal |
35 val kind = Keyword.thy_goal |
36 in |
36 in |
37 OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
37 Outer_Syntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
38 kind prove_prop_parser |
38 kind prove_prop_parser |
39 end |
39 end |
40 *} |
40 *} |
41 |
41 |
42 ML {* |
42 ML {* |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
53 in |
53 in |
54 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
54 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
55 end |
55 end |
56 |
56 |
57 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
57 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
58 |
58 |
59 in |
59 in |
60 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
60 Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
61 OuterKeyword.thy_goal (parser >> setup_proof) |
61 Keyword.thy_goal (parser >> setup_proof) |
62 end*} |
62 end*} |
63 |
63 |
64 |
64 |
65 (* |
|
66 ML {* |
|
67 let |
|
68 val do_nothing = Scan.succeed (Local_Theory.theory I) |
|
69 val kind = OuterKeyword.thy_decl |
|
70 in |
|
71 OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing |
|
72 end |
|
73 *}*) |
|
74 |
65 |
75 end |
66 end |