# HG changeset patch
# User wenzelm
# Date 954421940 -7200
# Node ID 63a0e1502e411ceeb52d30be8e3c361d7d4e7162
# Parent  87cddace4432e69325d8c7a2a9ba8b23a2ad9aa4
added 'moreover' and 'ultimately';

diff -r 87cddace4432 -r 63a0e1502e41 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Mar 30 15:11:48 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Mar 30 15:12:20 2000 +0200
@@ -47,10 +47,14 @@
 
 \section{Calculational proof}\label{sec:calculation}
 
-\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
+\indexisarcmd{also}\indexisarcmd{finally}
+\indexisarcmd{moreover}\indexisarcmd{ultimately}
+\indexisaratt{trans}
 \begin{matharray}{rcl}
   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
+  \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
+  \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
   trans & : & \isaratt \\
 \end{matharray}
 
@@ -62,12 +66,14 @@
 final $calculation$ by forward chaining towards the next goal statement.  Both
 commands require valid current facts, i.e.\ may occur only after commands that
 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
-$\HAVENAME$, $\SHOWNAME$ etc.
+$\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are
+similar to $\ALSO$ and $\FINALLY$, but only collect further results in
+$calculation$ without applying any rules yet.
 
 Also note that the automatic term abbreviation ``$\dots$'' has its canonical
-application with calculational proofs.  It automatically refers to the
-argument\footnote{The argument of a curried infix expression is its right-hand
-  side.} of the preceding statement.
+application with calculational proofs.  It refers to the argument\footnote{The
+  argument of a curried infix expression is its right-hand side.} of the
+preceding statement.
 
 Isabelle/Isar calculations are implicitly subject to block structure in the
 sense that new threads of calculational reasoning are commenced for any new
@@ -75,9 +81,24 @@
 being able to nest calculations, there is no separate \emph{begin-calculation}
 command required.
 
+\medskip
+
+The Isar calculation proof commands may be defined as
+follows:\footnote{Internal bookkeeping such as proper handling of
+  block-structure has been suppressed.}
+\begin{matharray}{rcl}
+  \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
+  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\
+  \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
+  \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
+  \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
+\end{matharray}
+
 \begin{rail}
   ('also' | 'finally') transrules? comment?
   ;
+  ('moreover' | 'ultimately') comment?
+  ;
   'trans' (() | 'add' | 'del')
   ;
 
@@ -102,6 +123,9 @@
   ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
   calculational proofs.
   
+\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
+  but collect results only, without applying rules.
+  
 \item [$trans$] declares theorems as transitivity rules.
 \end{descr}
 
diff -r 87cddace4432 -r 63a0e1502e41 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Thu Mar 30 15:11:48 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Thu Mar 30 15:12:20 2000 +0200
@@ -58,10 +58,16 @@
   \ALSO@0 & \approx & \NOTE{calculation}{this} \\
   \ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
   \FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
-  \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi}~~\text{(permissive assumption)} \\
-  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t}~~\text{(definitional assumption)} \\
-  \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi}~~\text{(generalized existence)} \\
-  \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi}~~\text{(named context)} \\[0.5ex]
+  \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
+  \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
+  \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
+%  & & \text{(permissive assumption)} \\
+  \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
+%  & & \text{(definitional assumption)} \\
+  \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
+%  & & \text{(generalized existence)} \\
+  \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
+%  & & \text{(named context)} \\[0.5ex]
   \SORRY & \approx & \BY{cheating} \\
 \end{matharray}