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