# HG changeset patch
# User wenzelm
# Date 936015107 -7200
# Node ID b7ca64c8fa64a4cd7bcfc6caf48e13f8db75f0b0
# Parent  f819265e267c2f9357383285b2f07efce9bf8c5c
'iff' attribute;

diff -r f819265e267c -r b7ca64c8fa64 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Aug 30 14:08:37 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Aug 30 14:11:47 1999 +0200
@@ -138,7 +138,7 @@
 
 Calculational proof is forward reasoning with implicit application of
 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
-an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
+an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
 results obtained by transitivity obtained together with the current facts.
 Command $\ALSO$ updates $calculation$ from the most recent result, while
 $\FINALLY$ exhibits the final result by forward chaining towards the next goal
@@ -243,7 +243,7 @@
 
 \subsection{Simplification methods}\label{sec:simp}
 
-\indexisarmeth{simp}\indexisarmeth{asm_simp}
+\indexisarmeth{simp}\indexisarmeth{asm-simp}
 \begin{matharray}{rcl}
   simp & : & \isarmeth \\
   asm_simp & : & \isarmeth \\
@@ -294,7 +294,8 @@
 
 \subsection{Forward simplification}
 
-\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
+\indexisaratt{simplify}\indexisaratt{asm-simplify}
+\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
 \begin{matharray}{rcl}
   simplify & : & \isaratt \\
   asm_simplify & : & \isaratt \\
@@ -348,7 +349,7 @@
 \subsection{Automatic methods}\label{sec:classical-auto}
 
 \indexisarmeth{blast}
-\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
+\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
 \begin{matharray}{rcl}
  blast & : & \isarmeth \\
  fast & : & \isarmeth \\
@@ -410,11 +411,13 @@
 
 \subsection{Modifying the context}\label{sec:classical-mod}
 
-\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
+\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
+\indexisaratt{iff}\indexisaratt{delrule}
 \begin{matharray}{rcl}
   intro & : & \isaratt \\
   elim & : & \isaratt \\
   dest & : & \isaratt \\
+  iff & : & \isaratt \\
   delrule & : & \isaratt \\
 \end{matharray}
 
@@ -429,6 +432,9 @@
   single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
   not applied in the search-oriented automatic methods).
   
+\item [$iff$] declares equations both as rewrite rules for the simplifier and
+  classical reasoning rules.
+
 \item [$delrule$] deletes introduction or elimination rules from the context.
   Note that destruction rules would have to be turned into elimination rules
   first, e.g.\ by using the $elimify$ attribute.