# HG changeset patch
# User wenzelm
# Date 863616517 -7200
# Node ID 3f7f4a7ae1d18bd0f26a5c023c0f7daf35843161
# Parent  3fff6839c616fddbe89e0bf1c3538c0dced53b0d
tuned;

diff -r 3fff6839c616 -r 3f7f4a7ae1d1 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Wed May 14 15:23:58 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Wed May 14 15:28:37 1997 +0200
@@ -1720,10 +1720,10 @@
 
 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
 
-In this example we define the type $\alpha~mylist$ again but this time we want
-to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
-\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
-after the constructor declarations as follows:
+In this example we define the type $\alpha~mylist$ again but this time
+we want to write {\tt []} for {\tt Nil} and we want to use infix
+notation \verb|#| for {\tt Cons}. To do this we simply add mixfix
+annotations after the constructor declarations as follows:
 \begin{ttbox}
 MyList = HOL +
   datatype 'a mylist =