author oheimb Wed, 30 May 2001 18:54:10 +0200 changeset 11332 11ab8c8ce694 parent 11331 6f747f6b8442 child 11333 d6b69fe04c1b
extended doc for iff attribute
--- 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