# HG changeset patch # User wenzelm # Date 1236679275 -3600 # Node ID bd38973f39e5ddd67351fe665153b92166cc5788 # Parent d03dd6301678fd0993448ddc1c0f5b42070cd191 updated generated file -- changed due to different treatmeant of type constraints in OptionalSugar.thy; diff -r d03dd6301678 -r bd38973f39e5 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue Mar 10 10:59:59 2009 +0100 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Tue Mar 10 11:01:15 2009 +0100 @@ -533,11 +533,11 @@ Likewise, \verb!concl! may be used as a style to show just the conclusion of a proposition. For example, take \verb!hd_Cons_tl!: \begin{center} - \isa{{\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} + \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} \end{center} To print just the conclusion, \begin{center} - \isa{hd\ {\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} + \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} \end{center} type \begin{quote}