--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Sep 01 00:45:24 2005 +0200
@@ -7,7 +7,6 @@
\endisadelimtheory
%
\isatagtheory
-\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
@@ -27,7 +26,7 @@
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
and seeing Isabelle typeset it for them:
\begin{isabelle}%
-{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}z{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ {\isacharparenleft}fst\ z{\isacharparenright}\ {\isacharparenleft}snd\ z{\isacharparenright}{\isacharparenright}%
+{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ x\ y{\isacharparenright}%
\end{isabelle}
No typos, no omissions, no sweat.
If you have not experienced that joy, read Chapter 4, \emph{Presenting
@@ -170,7 +169,6 @@
\endisadelimML
%
\isatagML
-\isamarkupfalse%
%
\endisatagML
{\isafoldML}%
@@ -481,7 +479,6 @@
\endisadelimML
%
\isatagML
-\isamarkupfalse%
%
\endisatagML
{\isafoldML}%
@@ -526,7 +523,6 @@
\endisadelimtheory
%
\isatagtheory
-\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%