1 theory Command |
1 theory Command |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
|
4 |
4 ML {* |
5 ML {* |
5 let |
6 let |
6 val do_nothing = Scan.succeed (LocalTheory.theory I) |
7 val do_nothing = Scan.succeed (LocalTheory.theory I) |
7 val kind = OuterKeyword.thy_goal |
8 val kind = OuterKeyword.thy_decl |
8 in |
9 in |
9 OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing |
10 OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing |
10 end |
11 end |
11 *} |
12 *} |
12 |
13 |
13 ML {* |
14 ML {* |
14 let |
15 let |
|
16 fun trace_prop str = |
|
17 LocalTheory.theory (fn lthy => (tracing str; lthy)) |
|
18 val trace_prop_parser = OuterParse.prop >> trace_prop |
|
19 val kind = OuterKeyword.thy_decl |
|
20 in |
|
21 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
|
22 kind trace_prop_parser |
|
23 end |
|
24 *} |
|
25 |
|
26 ML {* |
|
27 let |
|
28 fun prove_prop str lthy = |
|
29 let |
|
30 val prop = Syntax.read_prop lthy str |
|
31 in |
|
32 Proof.theorem_i NONE (K I) [[(prop,[])]] lthy |
|
33 end; |
|
34 val prove_prop_parser = OuterParse.prop >> prove_prop |
|
35 val kind = OuterKeyword.thy_goal |
|
36 in |
|
37 OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
|
38 kind prove_prop_parser |
|
39 end |
|
40 *} |
|
41 |
|
42 ML {* |
|
43 val r = ref (NONE:(unit -> term) option) |
|
44 *} |
|
45 ML {* |
|
46 let |
|
47 fun setup_proof (txt, pos) lthy = |
|
48 let |
|
49 val trm = ML_Context.evaluate lthy true ("r", r) txt |
|
50 in |
|
51 Proof.theorem_i NONE (K I) [[(trm,[])]] lthy |
|
52 end; |
|
53 |
|
54 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
|
55 |
|
56 val kind = OuterKeyword.thy_goal |
|
57 in |
|
58 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
|
59 kind setup_proof_parser |
|
60 end |
|
61 *} |
|
62 |
|
63 (* |
|
64 ML {* |
|
65 let |
15 val do_nothing = Scan.succeed (LocalTheory.theory I) |
66 val do_nothing = Scan.succeed (LocalTheory.theory I) |
16 val kind = OuterKeyword.thy_decl |
67 val kind = OuterKeyword.thy_decl |
17 in |
68 in |
18 OuterSyntax.local_theory "simple_induct" "description of foobar" kind do_nothing |
69 OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing |
19 end |
70 end |
20 *} |
71 *}*) |
21 |
72 |
22 end |
73 end |