--- a/doc-src/IsarRef/Thy/Generic.thy Mon Apr 16 19:38:48 2012 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon Apr 16 21:37:08 2012 +0200
@@ -129,7 +129,8 @@
@{attribute_def THEN} & : & @{text attribute} \\
@{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
@{attribute_def unfolded} & : & @{text attribute} \\
- @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def folded} & : & @{text attribute} \\
+ @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
@{attribute_def rotated} & : & @{text attribute} \\
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\
@{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
@@ -167,6 +168,11 @@
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
definitions throughout a rule.
+ \item @{attribute abs_def} turns an equation of the form @{prop "f x
+ y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method
+ simp} or @{method unfold} steps always expand it. This also works
+ for object-logic equality.
+
\item @{attribute rotated}~@{text n} rotate the premises of a
theorem by @{text n} (default 1).