# HG changeset patch
# User wenzelm
# Date 1334605028 -7200
# Node ID c78c6e1ec75d35bcefd46e20e567638eb2667381
# Parent  a43f207f216f82f2a8c3bf2a79163e999cd9a91e
document attribute "abs_def";

diff -r a43f207f216f -r c78c6e1ec75d doc-src/IsarRef/Thy/Generic.thy
--- 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).
 
diff -r a43f207f216f -r c78c6e1ec75d doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Apr 16 19:38:48 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Apr 16 21:37:08 2012 +0200
@@ -217,7 +217,8 @@
     \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
     \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
     \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
-    \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\[0.5ex]
+    \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\
+    \indexdef{}{attribute}{abs\_def}\hypertarget{attribute.abs-def}{\hyperlink{attribute.abs-def}{\mbox{\isa{abs{\isaliteral{5F}{\isacharunderscore}}def}}}} & : & \isa{attribute} \\[0.5ex]
     \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isa{attribute} \\
     \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}format}}}} & : & \isa{attribute} \\
     \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
@@ -283,6 +284,9 @@
   \item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand and fold back again the given
   definitions throughout a rule.
 
+  \item \hyperlink{attribute.abs-def}{\mbox{\isa{abs{\isaliteral{5F}{\isacharunderscore}}def}}} turns an equation of the form \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ y\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} into \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}}, which ensures that \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.unfold}{\mbox{\isa{unfold}}} steps always expand it.  This also works
+  for object-logic equality.
+
   \item \hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n} rotate the premises of a
   theorem by \isa{n} (default 1).