--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Feb 16 11:00:47 2007 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Feb 16 11:01:16 2007 +0100
@@ -196,6 +196,21 @@
the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again
displayed with a horizontal line, which looks at least unusual.
+
+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!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}\isastyle
+@{thm[mode=Axiom] refl} {\sc refl}
+\end{center}
+
+
+
*}
subsection{*If-then*}