equal
deleted
inserted
replaced
12 val add_thm: string -> thm -> Context.generic -> Context.generic |
12 val add_thm: string -> thm -> Context.generic -> Context.generic |
13 val del_thm: string -> thm -> Context.generic -> Context.generic |
13 val del_thm: string -> thm -> Context.generic -> Context.generic |
14 val add: string -> attribute |
14 val add: string -> attribute |
15 val del: string -> attribute |
15 val del: string -> attribute |
16 val check: Proof.context -> string * Position.T -> string |
16 val check: Proof.context -> string * Position.T -> string |
17 val declare: binding -> string list -> string -> |
17 val declare: binding -> string -> local_theory -> string * local_theory |
18 local_theory -> string * local_theory |
|
19 end; |
18 end; |
20 |
19 |
21 structure Named_Theorems: NAMED_THEOREMS = |
20 structure Named_Theorems: NAMED_THEOREMS = |
22 struct |
21 struct |
23 |
22 |
86 end; |
85 end; |
87 |
86 |
88 |
87 |
89 (* declaration *) |
88 (* declaration *) |
90 |
89 |
91 fun declare binding raw_extends descr lthy = |
90 fun declare binding descr lthy = |
92 let |
91 let |
93 val name = Local_Theory.full_name lthy binding; |
92 val name = Local_Theory.full_name lthy binding; |
94 val extends = map (fn s => check lthy (s, Position.none)) raw_extends; |
|
95 val description = |
93 val description = |
96 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
94 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
97 val lthy' = lthy |
95 val lthy' = lthy |
98 |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |
96 |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |
99 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |
97 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |
100 |> Local_Theory.add_thms_dynamic (binding, |
98 |> Local_Theory.add_thms_dynamic (binding, fn context => content context name) |
101 fn context => maps (content context) (extends @ [name])) |
|
102 |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description |
99 |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description |
103 in (name, lthy') end; |
100 in (name, lthy') end; |
104 |
101 |
105 |
102 |
106 (* ML antiquotation *) |
103 (* ML antiquotation *) |