doc-src/LaTeXsugar/Sugar/document/Sugar.tex

 \begin{quote}
 \verb!\begin{center}!\\
 \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:
 \begin{center}
 \isa{\mbox{}\inferrule{\mbox{A\ {\isasymlongrightarrow}\ B}\\\ \mbox{B\ {\isasymlongrightarrow}\ C}\\\ \mbox{C\ {\isasymlongrightarrow}\ D}\\\ \mbox{D\ {\isasymlongrightarrow}\ E}\\\ \mbox{E\ {\isasymlongrightarrow}\ F}\\\ \mbox{F\ {\isasymlongrightarrow}\ G}\\\ \mbox{G\ {\isasymlongrightarrow}\ H}\\\ \mbox{H\ {\isasymlongrightarrow}\ I}\\\ \mbox{I\ {\isasymlongrightarrow}\ J}\\\ \mbox{J\ {\isasymlongrightarrow}\ K}}{\mbox{A\ {\isasymlongrightarrow}\ K}}}

 
 
 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%
 }

 \isamarkupsection{Proofs%
 }
 \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
 %
 \isadelimproof
 %

 \begin{quote}
 \small
 \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 -!\\
 \verb!  -- "pretty trivial"!\\
 \verb!  show True by force!\\

 \verb!text_raw {!\verb!*!\\
 \verb!  \end{minipage}\end{center}!\\
 \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%
 %
 \isamarkupsection{Styles\label{sec:styles}%
 }