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 (Local_Theory.theory I) |
7 val do_nothing = Scan.succeed (Local_Theory.background_theory I) |
8 val kind = Keyword.thy_decl |
8 val kind = Keyword.thy_decl |
9 in |
9 in |
10 Outer_Syntax.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.background_theory (fn lthy => (tracing str; lthy)) |
18 val trace_prop_parser = Parse.prop >> trace_prop |
18 val trace_prop_parser = Parse.prop >> trace_prop |
19 val kind = Keyword.thy_decl |
19 val kind = Keyword.thy_decl |
20 in |
20 in |
21 Outer_Syntax.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 |