author wenzelm Wed, 14 May 1997 15:28:37 +0200 changeset 3181 3f7f4a7ae1d1 parent 3180 3fff6839c616 child 3182 3270d7bca923
tuned;
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- 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 =