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.
add missing attributes
authorkuncar
Mon, 24 Feb 2014 18:12:39 +0100
changeset 55720 f3a2931a6656
parent 55719 cdddd073bff8
child 55721 1c2cfc06c96a
add missing attributes
src/Pure/Isar/code.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/code.ML	Mon Feb 24 16:56:04 2014 +0000
+++ b/src/Pure/Isar/code.ML	Mon Feb 24 18:12:39 2014 +0100
@@ -47,6 +47,8 @@
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
   val add_abs_eqn: thm -> theory -> theory
+  val add_abs_eqn_attribute: attribute
+  val add_abs_eqn_attrib: Attrib.src
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
@@ -1121,6 +1123,10 @@
 
 fun add_abs_eqn raw_thm thy = gen_add_abs_eqn (mk_abs_eqn thy raw_thm) thy;
 
+val add_abs_eqn_attribute = Thm.declaration_attribute
+  (fn thm => Context.mapping (add_abs_eqn thm) I);
+val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+
 fun add_eqn_maybe_abs thm thy =
   case mk_eqn_maybe_abs thy thm
    of SOME (eqn, NONE) => gen_add_eqn false eqn thy
isabelle