author oheimb Mon Jul 23 13:50:23 2001 +0200 (2001-07-23) changeset 11442 8682a88c3d6a parent 11441 54b236801671 child 11443 77ed7e2b56c8
slight improvement for iff attribute
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Jul 22 21:31:37 2001 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Jul 23 13:50:23 2001 +0200
1.3 @@ -837,14 +837,15 @@
1.4    methods such as $rule$).
1.5  \item [$rule~del$] deletes introduction, elimination, or destruction rules from
1.6    the context.
1.7 -\item [$iff$] declares a safe'' rule to the context in several ways.
1.8 -  The rule is declared as a rewrite rule to the Simplifier. Furthermore, it is
1.9 +\item [$iff$] declares a (possibly conditional) safe'' rule to the context in
1.10 +  several ways.   The rule is declared as a rewrite rule to the Simplifier.
1.11 +  Furthermore, it is
1.12    declared in several ways (depending on its structure) to the Classical
1.13    Reasoner for aggressive use, which would normally be indicated by !'').
1.14    If the rule is an equivalence, the two corresponding implications are
1.15    declared as introduction and destruction rules. Otherwise, a warning is issued
1.16    and if the rule is an inequality, the corresponding negation elimination rule
1.17 -  is declared, else the rule itself is declared as an introduction.
1.18 +  is declared, else the rule itself is declared as an introduction rule.
1.19
1.20    The ?'' version of $iff$ declares extra'' Classical Reasoner rules only,
1.21    and omits the Simplifier declaration.  Thus the declaration does not have