--- 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
+(*>*)