--- a/doc-src/IsarRef/generic.tex Thu Dec 07 16:23:10 2000 +0100
+++ b/doc-src/IsarRef/generic.tex Thu Dec 07 17:09:15 2000 +0100
@@ -201,7 +201,8 @@
state, using Isar proof language notation. This is a diagnostic command;
$undo$ does not apply.
\item [$case_names~\vec c$] declares names for the local contexts of premises
- of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
+ of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
+ premises.
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
premises $1, \dots, n$ of some theorem. An empty list of names may be given
to skip positions, leaving the present parameters unchanged.