--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 31 12:16:24 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue May 31 12:16:42 2005 +0200
@@ -43,7 +43,10 @@
\item Should you need additional \LaTeX\ packages (the text will tell
you so), you include them at the beginning of your \LaTeX\ document,
-typically in \texttt{root.tex}.
+typically in \texttt{root.tex}. For a start, you should
+\verb!\usepackage{amssymb}! --- otherwise typesetting
+\isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} will fail because the AMS symbol
+\isa{{\isasymnexists}} is missing.
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -57,6 +60,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
+The formula \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} is typeset as \isa{{\isasymnexists}x{\isachardot}\ P\ x}.
+
The predefined constructs \isa{if}, \isa{let} and
\isa{case} are set in sans serif font to distinguish them from
other functions. This improves readability:
@@ -224,14 +229,42 @@
\begin{theorem}
\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{longpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longerpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longestpremise}\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
\end{theorem}
-In which case you should use \texttt{mode=IfThenNoBox} instead of
-\texttt{mode=IfThen}:
+In which case you should use \texttt{IfThenNoBox} instead of
+\texttt{IfThen}:
\begin{theorem}
\isa{{\rmfamily\upshape\normalsize{}If\,}\ longpremise\ {\rmfamily\upshape\normalsize \,and\,}\ longerpremise\ {\rmfamily\upshape\normalsize \,and\,}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\rmfamily\upshape\normalsize \,and\,}\ longestpremise\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
\end{theorem}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Doing it yourself%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+If for some reason you want or need to present theorems your
+own way, you can extract the premises and the conclusion explicitly
+and combine them as you like:
+\begin{itemize}
+\item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
+prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
+\item \verb!@!\verb!{thm_style conclusion! $thm$\verb!}!
+prints the conclusion of $thm$.
+\end{itemize}
+For example, ``from \isa{Q} and
+\isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
+is produced by
+\begin{quote}
+\verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
+\verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm_style conclusion conjI}!
+\end{quote}
+Thus you can rearrange or hide premises and typeset the theorem as you like.
+The \verb!thm_style! antiquotation is a general mechanism explained
+in \S\ref{sec:styles}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Patterns%
}
\isamarkuptrue%
@@ -320,7 +353,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Styles%
+\isamarkupsubsection{Styles\label{sec:styles}%
}
\isamarkuptrue%
%
--- a/doc-src/LaTeXsugar/Sugar/document/isabellesym.sty Tue May 31 12:16:24 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/isabellesym.sty Tue May 31 12:16:42 2005 +0200
@@ -220,6 +220,7 @@
\newcommand{\isasymOr}{\isamath{\bigvee}}
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
\newcommand{\isasymturnstile}{\isamath{\vdash}}
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Tue May 31 12:16:24 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Tue May 31 12:16:42 2005 +0200
@@ -3,7 +3,7 @@
% further packages required for unusual symbols (see also isabellesym.sty)
% use only when needed
-%\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
+\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
% \<sqsupset>, \<mho>, \<Join>,
% \<lhd>, \<lesssim>, \<greatersim>,
% \<lessapprox>, \<greaterapprox>,