--- a/doc-src/IsarRef/conversion.tex Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/conversion.tex Tue Sep 04 21:10:57 2001 +0200
@@ -223,9 +223,9 @@
Note that the above scheme repeats the text of premises $\phi@1$, \dots, while
the conclusion $\psi$ is referenced via the automatic text abbreviation
$\Var{thesis}$. The assumption context may be invoked in a less verbose
-manner as well, using ``$\CASE{antecedent}$'' instead of
+manner as well, using ``$\CASE{rule_context}$'' instead of
``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above. Then the list of \emph{all}
-premises is bound to the name $antecedent$; Isar does not provide a way to
+premises is bound to the name $rule_context$; Isar does not provide a way to
destruct lists into single items, though.
\medskip In practice, actual rules are often rather direct consequences of