# HG changeset patch
# User nipkow
# Date 1188568579 -7200
# Node ID 7840f760a7446306738102179eed9d3138f9b054
# Parent  65f3b37f80b7d53631b51f5b1e63d3f6c0f31233
explained \isatstyle(minor)

diff -r 65f3b37f80b7 -r 7840f760a744 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Aug 31 12:24:00 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Aug 31 15:56:19 2007 +0200
@@ -181,27 +181,25 @@
 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
 \verb!\end{center}!
 \end{quote}
-It is not recommended to use the standard \texttt{display} attribute
+It is not recommended to use the standard \texttt{display} option
 together with \texttt{Rule} because centering does not work and because
 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
 clash.
 
 Of course you can display multiple rules in this fashion:
 \begin{quote}
-\verb!\begin{center}\isastyle!\\
+\verb!\begin{center}!\\
 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
 \verb!\end{center}!
 \end{quote}
 yields
-\begin{center}\isastyle
+\begin{center}\small
 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
 \end{center}
-Note that we included \verb!\isastyle! to obtain
-the smaller font that otherwise comes only with \texttt{display}.
 
 The \texttt{mathpartir} package copes well if there are too many
 premises for one line:
@@ -218,20 +216,44 @@
 In case you print theorems without premises no rule will be printed by the
 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
 \begin{quote}
-\verb!\begin{center}\isastyle!\\
+\verb!\begin{center}!\\
 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
 \verb!\end{center}!
 \end{quote}
 yields
-\begin{center}\isastyle
+\begin{center}
 @{thm[mode=Axiom] refl} {\sc refl} 
 \end{center}
-
-
-
 *}
 
-subsection{*If-then*}
+subsection "Displays and font sizes"
+
+text{* When displaying theorems with the \texttt{display} option, e.g.
+\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
+set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
+which is also the style that regular theory text is set in, e.g. *}
+
+lemma "t = t"
+(*<*)oops(*>*)
+
+text{* \noindent Otherwise \verb!\isastyleminor! is used,
+which does not modify the font size (assuming you stick to the default
+\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
+normal font size throughout your text, include
+\begin{quote}
+\verb!\renewcommand{\isastyle}{\isastyleminor}!
+\end{quote}
+in \texttt{root.tex}. On the other hand, if you like the small font,
+just put \verb!\isastyle! in front of the text in question,
+e.g.\ at the start of one of the center-environments above.
+
+The advantage of the display option is that you can display a whole
+list of theorems in one go. For example,
+\verb!@!\verb!{thm[display] foldl.simps}!
+generates @{thm[display] foldl.simps}
+*}
+
+subsection "If-then"
 
 text{* If you prefer a fake ``natural language'' style you can produce
 the body of
@@ -303,19 +325,16 @@
 
 section "Proofs"
 
-text {*
-  Full proofs, even if written in beautiful Isar style, are likely to
-  be too long and detailed to be included in conference papers, but
-  some key lemmas might be of interest.
-
-  It is usually easiest to put them in figures like the one in Fig.\
-  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
-  command:
+text {* Full proofs, even if written in beautiful Isar style, are
+likely to be too long and detailed to be included in conference
+papers, but some key lemmas might be of interest.
+It is usually easiest to put them in figures like the one in Fig.\
+\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
 *}
 text_raw {*
   \begin{figure}
   \begin{center}\begin{minipage}{0.6\textwidth}  
-  \isastyle\isamarkuptrue
+  \isastyleminor\isamarkuptrue
 *}
 lemma True
 proof -
@@ -334,7 +353,7 @@
 \verb!text_raw {!\verb!*!\\
 \verb!  \begin{figure}!\\
 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb!  \isastyle\isamarkuptrue!\\
+\verb!  \isastyleminor\isamarkuptrue!\\
 \verb!*!\verb!}!\\
 \verb!lemma True!\\
 \verb!proof -!\\
@@ -347,7 +366,8 @@
 \verb!  \end{figure}!\\
 \verb!*!\verb!}!
 \end{quote}
-  
+
+Other theory text, e.g.\ definitions, can be put in figures, too.
 *}
 
 section {*Styles\label{sec:styles}*}
diff -r 65f3b37f80b7 -r 7840f760a744 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Aug 31 12:24:00 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Aug 31 15:56:19 2007 +0200
@@ -240,27 +240,25 @@
 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
 \verb!\end{center}!
 \end{quote}
-It is not recommended to use the standard \texttt{display} attribute
+It is not recommended to use the standard \texttt{display} option
 together with \texttt{Rule} because centering does not work and because
 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
 clash.
 
 Of course you can display multiple rules in this fashion:
 \begin{quote}
-\verb!\begin{center}\isastyle!\\
+\verb!\begin{center}!\\
 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
 \verb!\end{center}!
 \end{quote}
 yields
-\begin{center}\isastyle
+\begin{center}\small
 \isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI} \\[1ex]
 \isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_1$} \qquad
 \isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_2$}
 \end{center}
-Note that we included \verb!\isastyle! to obtain
-the smaller font that otherwise comes only with \texttt{display}.
 
 The \texttt{mathpartir} package copes well if there are too many
 premises for one line:
@@ -276,17 +274,67 @@
 In case you print theorems without premises no rule will be printed by the
 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
 \begin{quote}
-\verb!\begin{center}\isastyle!\\
+\verb!\begin{center}!\\
 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
 \verb!\end{center}!
 \end{quote}
 yields
-\begin{center}\isastyle
+\begin{center}
 \isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isacharequal}\ t}}} {\sc refl} 
 \end{center}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Displays and font sizes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When displaying theorems with the \texttt{display} option, e.g.
+\verb!@!\verb!{thm[display] refl}! \begin{isabelle}%
+t\ {\isacharequal}\ t%
+\end{isabelle} the theorem is
+set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
+which is also the style that regular theory text is set in, e.g.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}t\ {\isacharequal}\ t{\isachardoublequoteclose}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Otherwise \verb!\isastyleminor! is used,
+which does not modify the font size (assuming you stick to the default
+\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
+normal font size throughout your text, include
+\begin{quote}
+\verb!\renewcommand{\isastyle}{\isastyleminor}!
+\end{quote}
+in \texttt{root.tex}. On the other hand, if you like the small font,
+just put \verb!\isastyle! in front of the text in question,
+e.g.\ at the start of one of the center-environments above.
+
+The advantage of the display option is that you can display a whole
+list of theorems in one go. For example,
+\verb!@!\verb!{thm[display] foldl.simps}!
+generates \begin{isabelle}%
+foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ a\isasep\isanewline%
+foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}\ {\isacharequal}\ foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs%
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{If-then%
 }
 \isamarkuptrue%
@@ -372,19 +420,17 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Full proofs, even if written in beautiful Isar style, are likely to
-  be too long and detailed to be included in conference papers, but
-  some key lemmas might be of interest.
-
-  It is usually easiest to put them in figures like the one in Fig.\
-  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
-  command:%
+Full proofs, even if written in beautiful Isar style, are
+likely to be too long and detailed to be included in conference
+papers, but some key lemmas might be of interest.
+It is usually easiest to put them in figures like the one in Fig.\
+\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{figure}
   \begin{center}\begin{minipage}{0.6\textwidth}  
-  \isastyle\isamarkuptrue
+  \isastyleminor\isamarkuptrue
 \isacommand{lemma}\isamarkupfalse%
 \ True\isanewline
 %
@@ -421,7 +467,7 @@
 \verb!text_raw {!\verb!*!\\
 \verb!  \begin{figure}!\\
 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb!  \isastyle\isamarkuptrue!\\
+\verb!  \isastyleminor\isamarkuptrue!\\
 \verb!*!\verb!}!\\
 \verb!lemma True!\\
 \verb!proof -!\\
@@ -433,7 +479,9 @@
 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
 \verb!  \end{figure}!\\
 \verb!*!\verb!}!
-\end{quote}%
+\end{quote}
+
+Other theory text, e.g.\ definitions, can be put in figures, too.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %