# HG changeset patch
# User wenzelm
# Date 910041515 -3600
# Node ID cdd2add0fd969aadcf321eb5bf3c8274962aa964
# Parent  dd83042c2f70cfa7fb9eb577ea7d2ba0409e32fb
oops;

diff -r dd83042c2f70 -r cdd2add0fd96 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Mon Nov 02 22:16:49 1998 +0100
+++ b/doc-src/Logics/HOL.tex	Mon Nov 02 22:18:35 1998 +0100
@@ -1950,8 +1950,8 @@
                             | Cons' (('a,'b) term) (('a,'b) term_list)
 \end{ttbox}
 Note however, that the type {\tt ('a,'b) term_list} and the constructors {\tt
-  Nil'} and {\tt Cons'} are not really introduced.  One can directly work the
-original (isomorphic) type {\tt (('a, 'b) term) list} and its existing
+  Nil'} and {\tt Cons'} are not really introduced.  One can directly work with
+the original (isomorphic) type {\tt (('a, 'b) term) list} and its existing
 constructors {\tt Nil} and {\tt Cons}. Thus, the structural induction rule for
 {\tt term} gets the form
 \[