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

 \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}}}
 \end{center}
 
 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%
 %
 \isamarkupsubsection{If-then%
 }