# HG changeset patch
# User kleing
# Date 1102074744 -3600
# Node ID 79f624f97f7fde972610ab261a350e5c0020f4dd
# Parent  ac18081228ae81d6d4a035d48911f0f6ce94159f
tuned

diff -r ac18081228ae -r 79f624f97f7f doc-src/LaTeXsugar/Sugar/OptionalSugar.thy
--- 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)
diff -r ac18081228ae -r 79f624f97f7f doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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}