10 val get: Proof.context -> string -> thm list |
10 val get: Proof.context -> string -> thm list |
11 val add_thm: string -> thm -> Context.generic -> Context.generic |
11 val add_thm: string -> thm -> Context.generic -> Context.generic |
12 val del_thm: string -> thm -> Context.generic -> Context.generic |
12 val del_thm: string -> thm -> Context.generic -> Context.generic |
13 val add: string -> attribute |
13 val add: string -> attribute |
14 val del: string -> attribute |
14 val del: string -> attribute |
15 val declare: binding -> string -> theory -> string * theory |
15 val declare: binding -> string -> local_theory -> string * local_theory |
16 end; |
16 end; |
17 |
17 |
18 structure Named_Theorems: NAMED_THEOREMS = |
18 structure Named_Theorems: NAMED_THEOREMS = |
19 struct |
19 struct |
20 |
20 |
57 val del = Thm.declaration_attribute o del_thm; |
57 val del = Thm.declaration_attribute o del_thm; |
58 |
58 |
59 |
59 |
60 (* declaration *) |
60 (* declaration *) |
61 |
61 |
62 fun declare binding descr thy = |
62 fun declare binding descr lthy = |
63 let |
63 let |
64 (* FIXME proper result from Global_Theory.add_thms_dynamic *) |
64 val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding; |
65 val naming = Name_Space.naming_of (Context.Theory thy); |
|
66 val name = Name_Space.full_name naming binding; |
|
67 |
|
68 val thy' = thy |
|
69 |> Global_Theory.add_thms_dynamic (binding, fn context => content context name); |
|
70 |
|
71 val description = |
65 val description = |
72 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
66 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
73 val thy'' = thy' |
67 val lthy' = lthy |
74 |> Context.theory_map (new_entry name) |
68 |> Local_Theory.background_theory |
75 |> Attrib.setup binding (Attrib.add_del (add name) (del name)) description; |
69 (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #> |
76 in (name, thy'') end; |
70 Attrib.setup binding (Attrib.add_del (add name) (del name)) description #> |
|
71 Context.theory_map (new_entry name)) |
|
72 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |
|
73 |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
|
74 let |
|
75 val binding' = Morphism.binding phi binding; |
|
76 val context' = |
|
77 context |> Context.mapping |
|
78 (Global_Theory.alias_fact binding' name) |
|
79 (fn ctxt => |
|
80 if Facts.defined (Proof_Context.facts_of ctxt) name |
|
81 then Proof_Context.fact_alias binding' name ctxt |
|
82 else ctxt); |
|
83 in context' end); |
|
84 in (name, lthy') end; |
77 |
85 |
78 val _ = |
86 val _ = |
79 Outer_Syntax.command @{command_spec "named_theorems"} |
87 Outer_Syntax.local_theory @{command_spec "named_theorems"} |
80 "declare named collection of theorems" |
88 "declare named collection of theorems" |
81 (Parse.binding -- Scan.optional Parse.text "" |
89 (Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr)); |
82 >> (fn (binding, descr) => Toplevel.theory (snd o declare binding descr))); |
|
83 |
90 |
84 |
91 |
85 (* ML antiquotation *) |
92 (* ML antiquotation *) |
86 |
93 |
87 val _ = Theory.setup |
94 val _ = Theory.setup |