# HG changeset patch
# User haftmann
# Date 1172846598 -3600
# Node ID 17827a3c02d08d0ff3a42cd2806bbb5ab5576c18
# Parent  4ebe883b02ff020ea2853526a127e1ac27ce4467
adjusted to latest changes

diff -r 4ebe883b02ff -r 17827a3c02d0 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Mar 02 15:43:17 2007 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Mar 02 15:43:18 2007 +0100
@@ -249,7 +249,20 @@
 
 Limitations: 1. Premises and conclusion must each not be longer than
 the line.  2. Premises that are \isa{{\isasymLongrightarrow}}-implications are again
-displayed with a horizontal line, which looks at least unusual.%
+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
+\isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isacharequal}\ t}}} {\sc refl} 
+\end{center}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %