Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export add/del_thm;
authorwenzelm
Thu, 20 Mar 2008 16:04:34 +0100
changeset 26363 9d95309f8069
parent 26362 d9ce159a41d1
child 26364 cb6f360ab425
export add/del_thm;
src/Pure/Tools/named_thms.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:32 2008 +0100
+++ b/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:34 2008 +0100
@@ -9,6 +9,8 @@
 sig
   val get: Proof.context -> thm list
   val pretty: Proof.context -> Pretty.T
+  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
@@ -30,8 +32,11 @@
 fun pretty ctxt =
   Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
 
-val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
-val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
+val add_thm = Data.map o Thm.add_thm;
+val del_thm = Data.map o Thm.del_thm;
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
 
 val setup =
   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
isabelle