# HG changeset patch
# User nipkow
# Date 1117534602 -7200
# Node ID 9bf4b6bf43720fd4a1e78cd1a9f641b66614af51
# Parent  999ca183b4c7009d43ed6c9028d9b98117f93c55
\nexists

diff -r 999ca183b4c7 -r 9bf4b6bf4372 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- 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%
 %
diff -r 999ca183b4c7 -r 9bf4b6bf4372 doc-src/LaTeXsugar/Sugar/document/isabellesym.sty
--- 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}}
diff -r 999ca183b4c7 -r 9bf4b6bf4372 doc-src/LaTeXsugar/Sugar/document/root.tex
--- 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>,