--- a/doc-src/IsarRef/refcard.tex Tue Mar 21 17:32:43 2000 +0100
+++ b/doc-src/IsarRef/refcard.tex Tue Mar 21 17:32:44 2000 +0100
@@ -58,14 +58,10 @@
\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]
+ \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}