author wenzelm Sun, 11 Feb 2001 16:31:21 +0100 changeset 11095 2ffaf1e1e101 parent 11094 b803ef642e60 child 11096 bedfd42db838
updated;
--- 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