Named collections of theorems in canonical (reverse) order: OLD VERSION.
*)
signature NAMED_THMS = sig val member: Proof.context -> thm -> bool val get: Proof.context -> thm list val add_thm: thm -> Context.generic -> Context.generic val del_thm: thm -> Context.generic -> Context.generic val add: attribute val del: attribute val setup: theory -> theory end;
functor Named_Thms(val name: binding val description: string): NAMED_THMS = struct
structure Data = Generic_Data
( type T = thm Item_Net.T; val empty = Thm.item_net; val merge = Item_Net.merge;
);
val member = Item_Net.member o Data.get o Context.Proof;
fun content context = map (Thm.transfer'' context) (Item_Net.content (Data.get context)); val get = content o Context.Proof;
val add_thm = Data.map o Item_Net.update o Thm.trim_context; val del_thm = Data.map o Item_Net.remove;
val add = Thm.declaration_attribute add_thm; val del = Thm.declaration_attribute del_thm;
val setup =
Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
Global_Theory.add_thms_dynamic (name, content);
end;
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
