doc-src/LaTeXsugar/Sugar/Sugar.thy
changeset 15368 79f624f97f7f
parent 15367 ac18081228ae
child 15373 cf912e83bf6f
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Dec 03 07:27:48 2004 +0100
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Dec 03 12:52:24 2004 +0100
     1.3 @@ -85,9 +85,6 @@
     1.4  line breaking behaviour:
     1.5  @{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
     1.6  
     1.7 -\item The same can be done for @{text"\<and>"}:
     1.8 -@{term[display]"term\<^isub>0 \<and> term\<^isub>1 \<and> term\<^isub>2 \<and> term\<^isub>3 \<and> term\<^isub>4 \<and> term\<^isub>5 \<and> term\<^isub>6 \<and> term\<^isub>7 \<and> term\<^isub>9 \<and> term\<^isub>1\<^isub>0 \<and> term\<^isub>1\<^isub>1"}
     1.9 -
    1.10  \end{itemize}
    1.11  *}
    1.12  
    1.13 @@ -172,7 +169,7 @@
    1.14  
    1.15  text {*
    1.16    The \verb!thm! antiquotation works nicely for proper theorems, but
    1.17 -  sets of equations as used in defintions are more difficult to
    1.18 +  sets of equations as used in definitions are more difficult to
    1.19    typeset nicely: for some reason people tend to prefer aligned 
    1.20    @{text "="} signs.
    1.21  
    1.22 @@ -252,8 +249,8 @@
    1.23  
    1.24    You can drive this game even further and extend the syntax of let
    1.25    bindings such that certain functions like @{term fst}, @{term hd}, 
    1.26 -  etc.\ are printed nicely. \texttt{OptionalSugar} provides the
    1.27 -  following pretty printing patterns:
    1.28 +  etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
    1.29 +  following:
    1.30    
    1.31    \begin{center}
    1.32    \begin{tabular}{l@ {~~produced by~~}l}