# HG changeset patch
# User nipkow
# Date 1117647615 -7200
# Node ID 749e6b68ca847fbe2bc7c54e12f737b41504cb65
# Parent  a55c796b1f7983aa7c733ed934aebebc621ba055
tuned

diff -r a55c796b1f79 -r 749e6b68ca84 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 18:29:03 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 01 19:40:15 2005 +0200
@@ -221,8 +221,7 @@
 @{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
 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.
@@ -415,4 +414,4 @@
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)