# HG changeset patch
# User nipkow
# Date 1117647626 -7200
# Node ID ef83d8e097baebfac0678cea8bd9bf7df18a55da
# Parent  749e6b68ca847fbe2bc7c54e12f737b41504cb65
*** empty log message ***

diff -r 749e6b68ca84 -r ef83d8e097ba doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 01 19:40:15 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jun 01 19:40:26 2005 +0200
@@ -255,8 +255,7 @@
 \isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
 is produced by
 \begin{quote}
-\verb!from !\verb!@!\verb!{thm_style prem2 conjI}!\\
-\verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
+\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
 \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
 \end{quote}
 Thus you can rearrange or hide premises and typeset the theorem as you like.