# HG changeset patch
# User wenzelm
# Date 976205355 -3600
# Node ID dc3eff1b755621ed7ba438ad7f459d7e660d8e63
# Parent  46bcddfe9e7b483a1d25355a46d916a003961ac9
tuned;

diff -r 46bcddfe9e7b -r dc3eff1b7556 doc-src/IsarRef/generic.tex
--- 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.