# HG changeset patch
# User oheimb
# Date 991241650 -7200
# Node ID 11ab8c8ce6944084680c5b7007886e6778666690
# Parent  6f747f6b84420fe0dd41cfc055b47d157b483519
extended doc for iff attribute

diff -r 6f747f6b8442 -r 11ab8c8ce694 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed May 30 10:48:59 2001 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed May 30 18:54:10 2001 +0200
@@ -66,7 +66,7 @@
 \end{matharray}
 
 Calculational proof is forward reasoning with implicit application of
-transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
+transitivity rules (such those of $=$, $\leq$, $<$).  Isabelle/Isar maintains
 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
 results obtained by transitivity composed with the current result.  Command
 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
@@ -830,17 +830,21 @@
   Classical Reasoner, which is also known as ``simpset'' internally
   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
-  destruct rules, respectively.  By default, rules are considered as
+  destruction rules, respectively.  By default, rules are considered as
   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   applied in the search-oriented automated methods, but only in single-step
   methods such as $rule$).
-\item [$rule~del$] deletes introduction, elimination, or destruct rules from
+\item [$rule~del$] deletes introduction, elimination, or destruction rules from
   the context.
-\item [$iff$] declares equivalence rules to the context.  The default behavior
-  is to declare a rewrite rule to the Simplifier, and the two corresponding
-  implications to the Classical Reasoner (as ``safe'' rules that are used
-  aggressively, which would normally be indicated by ``!'').
+\item [$iff$] declares a ``safe'' rule to the context in several ways. 
+  The rule is declared as a rewrite rule to the Simplifier. Furthermore, it is 
+  declared in several ways (depending on its structure) to the Classical 
+  Reasoner for aggressive use, which would normally be indicated by ``!'').
+  If the rule is an equivalence, the two corresponding implications are 
+  declared as introduction and destruction rules. If it is an inequality, the
+  corresponding elimination rule is declared. Otherwise, a warning is issued
+  and the rule is delcared as an intruction.
   
   The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
   and omits the Simplifier declaration.  Thus the declaration does not have