equal
deleted
inserted
replaced
116 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as |
116 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as |
117 follows. The first occurrence of $\ALSO$ in some calculational thread |
117 follows. The first occurrence of $\ALSO$ in some calculational thread |
118 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
118 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
119 level of block-structure updates $calculation$ by some transitivity rule |
119 level of block-structure updates $calculation$ by some transitivity rule |
120 applied to $calculation$ and $this$ (in that order). Transitivity rules are |
120 applied to $calculation$ and $this$ (in that order). Transitivity rules are |
121 picked from the current context plus those given as explicit arguments (the |
121 picked from the current context, unless alternative rules are given as |
122 latter have precedence). |
122 explicit arguments. |
123 |
123 |
124 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
124 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
125 $\ALSO$, and concludes the current calculational thread. The final result |
125 $\ALSO$, and concludes the current calculational thread. The final result |
126 is exhibited as fact for forward chaining towards the next goal. Basically, |
126 is exhibited as fact for forward chaining towards the next goal. Basically, |
127 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
127 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |