# HG changeset patch
# User kleing
# Date 1107398035 -3600
# Node ID 7c1f6e84f4ade1cbe913c45de3c61c50db04d4f7
# Parent  2a183ef25fb1b27fa0a3af9fa7c4c301cc4290c7
Document now applies to devel version (and Isabelle 2005)

diff -r 2a183ef25fb1 -r 7c1f6e84f4ad doc-src/LaTeXsugar/IsaMakefile
--- a/doc-src/LaTeXsugar/IsaMakefile	Wed Feb 02 18:20:31 2005 +0100
+++ b/doc-src/LaTeXsugar/IsaMakefile	Thu Feb 03 03:33:55 2005 +0100
@@ -23,8 +23,7 @@
 
 $(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \
   Sugar/document/root.tex Sugar/document/root.bib \
-  ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptionalSugar.thy \
-  ../../Distribution/lib/texinputs/sugar.sty
+  ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptionalSugar.thy 
 	@$(USEDIR) HOL Sugar
 
 
diff -r 2a183ef25fb1 -r 7c1f6e84f4ad doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Feb 02 18:20:31 2005 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Feb 03 03:33:55 2005 +0100
@@ -182,7 +182,7 @@
   typeset nicely: for some reason people tend to prefer aligned 
   @{text "="} signs.
 
-  Isabelle2005 will have a nice mechanism for that, namely the two
+  Isabelle2005 has a nice mechanism for this, namely the two
   antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
 
   \begin{center}
@@ -211,37 +211,6 @@
   try to be smart about the interpretation of the theorem they
   print, they work just as well for meta equality @{text "\<equiv>"} and other
   binary operators like @{text "<"}.
-
-  Should you lack both the development version of Isabelle and a time
-  machine, you can still try to simulate the effect using the equation syntax
-  in \texttt{sugar.sty} and \texttt{OptionalSugar}.
-  
-  \begin{center}
-  \begin{tabular}{l@ { }l@ { }l}
-  \setcounter{isatabs}{0}%
-  @{thm [mode=tab] foldl_Nil[no_vars]}\nl
-  @{thm [mode=tab] foldl_Cons[no_vars]}
-  \end{tabular}
-  \end{center}
-
-  \noindent 
-  is produced by:
-
-\begin{quote}
-  \verb!\begin{center}!\\
-  \verb!\begin{tabular}{l@ { }l@ { }l}!\\
-  \verb!\setcounter{isatabs}{0}%!\\
-  \verb!@!\verb!{thm [mode=tab] foldl_Nil[no_vars]}\nl!\\
-  \verb!@!\verb!{thm [mode=tab] foldl_Cons[no_vars]}!\\
-  \verb!\end{tabular}!\\
-  \verb!\end{center}!
-\end{quote}
-
-  \noindent
-  These \LaTeX\ macros are not as flexible as the antiquotations
-  above, they only work for proper equations and definitions and they
-  only work correctly if the left hand side does not contain any
-  @{text "="} signs.
 *}
 
 subsection "Patterns"