--- 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
--- 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"