equal
deleted
inserted
replaced
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 let |
6 let |
7 val do_nothing = Scan.succeed (LocalTheory.theory I) |
7 val do_nothing = Scan.succeed (Local_Theory.theory I) |
8 val kind = OuterKeyword.thy_decl |
8 val kind = OuterKeyword.thy_decl |
9 in |
9 in |
10 OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing |
10 OuterSyntax.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 LocalTheory.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 = OuterParse.prop >> trace_prop |
19 val kind = OuterKeyword.thy_decl |
19 val kind = OuterKeyword.thy_decl |
20 in |
20 in |
21 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
21 OuterSyntax.local_theory "foobar_trace" "traces a proposition" |
22 kind trace_prop_parser |
22 kind trace_prop_parser |
43 val r = Unsynchronized.ref (NONE:(unit -> term) option) |
43 val r = Unsynchronized.ref (NONE:(unit -> term) option) |
44 *} |
44 *} |
45 ML{* |
45 ML{* |
46 let |
46 let |
47 fun after_qed thm_name thms lthy = |
47 fun after_qed thm_name thms lthy = |
48 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
48 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
49 |
49 |
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
51 let |
51 let |
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 |
63 |
63 |
64 |
64 |
65 (* |
65 (* |
66 ML {* |
66 ML {* |
67 let |
67 let |
68 val do_nothing = Scan.succeed (LocalTheory.theory I) |
68 val do_nothing = Scan.succeed (Local_Theory.theory I) |
69 val kind = OuterKeyword.thy_decl |
69 val kind = OuterKeyword.thy_decl |
70 in |
70 in |
71 OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing |
71 OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing |
72 end |
72 end |
73 *}*) |
73 *}*) |