--- a/NEWS Tue Mar 13 14:44:27 2012 +0100
+++ b/NEWS Tue Mar 13 16:22:18 2012 +0100
@@ -43,6 +43,11 @@
*** Pure ***
+* Attribute "abs_def" turns an equation of the form "f x y == t" into
+"f == %x y. t", which ensures that "simp" or "unfold" steps always
+expand it. This also works for object-logic equality. (Formerly
+undocumented feature.)
+
* Discontinued old "prems" fact, which used to refer to the accidental
collection of foundational premises in the context (marked as legacy
since Isabelle2011).
--- a/src/Pure/Isar/attrib.ML Tue Mar 13 14:44:27 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Mar 13 16:22:18 2012 +0100
@@ -399,8 +399,10 @@
setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
"declaration of definitional transformations" #>
- setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
- "abstract over free variables of a definition"));
+ setup (Binding.name "abs_def")
+ (Scan.succeed (Thm.rule_attribute (fn context =>
+ Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+ "abstract over free variables of definitionial theorem"));