# HG changeset patch
# User wenzelm
# Date 981905481 -3600
# Node ID 2ffaf1e1e101a584a80ebf70414c2eecd49e2402
# Parent  b803ef642e609598583bde7e59f5cfb6dfc1be17
updated;

diff -r b803ef642e60 -r 2ffaf1e1e101 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Feb 11 13:26:23 2001 +0100
+++ b/doc-src/IsarRef/generic.tex	Sun Feb 11 16:31:21 2001 +0100
@@ -118,8 +118,8 @@
   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
   level of block-structure updates $calculation$ by some transitivity rule
   applied to $calculation$ and $this$ (in that order).  Transitivity rules are
-  picked from the current context plus those given as explicit arguments (the
-  latter have precedence).
+  picked from the current context, unless alternative rules are given as
+  explicit arguments.
 
 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
   $\ALSO$, and concludes the current calculational thread.  The final result