--- a/doc-src/LaTeXsugar/Sugar/OptionalSugar.thy Fri Dec 03 07:27:48 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/OptionalSugar.thy Fri Dec 03 12:52:24 2004 +0100
@@ -10,14 +10,6 @@
"appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
-(* and *)
-syntax (latex output)
- "_andL" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<^raw:\isasymand>" 35)
-translations
- "_andL A B" <= "A \<and> B"
- "_andL (_andL A B) C" <= "_andL A (_andL B C)"
-
-
(* aligning equations *)
syntax (tab output)
"op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Dec 03 07:27:48 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Dec 03 12:52:24 2004 +0100
@@ -85,9 +85,6 @@
line breaking behaviour:
@{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"}
-\item The same can be done for @{text"\<and>"}:
-@{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"}
-
\end{itemize}
*}
@@ -172,7 +169,7 @@
text {*
The \verb!thm! antiquotation works nicely for proper theorems, but
- sets of equations as used in defintions are more difficult to
+ sets of equations as used in definitions are more difficult to
typeset nicely: for some reason people tend to prefer aligned
@{text "="} signs.
@@ -252,8 +249,8 @@
You can drive this game even further and extend the syntax of let
bindings such that certain functions like @{term fst}, @{term hd},
- etc.\ are printed nicely. \texttt{OptionalSugar} provides the
- following pretty printing patterns:
+ etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
+ following:
\begin{center}
\begin{tabular}{l@ {~~produced by~~}l}