# HG changeset patch # User paulson # Date 1111152710 -3600 # Node ID b098158a3f394ded88932b09e6872066bb6af91b # Parent ab90e95ae02efa78663300f2df660643839b9d26 auto update diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Mar 18 14:31:50 2005 +0100 @@ -137,6 +137,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Mar 18 14:31:50 2005 +0100 @@ -135,12 +135,14 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Mar 18 14:31:50 2005 +0100 @@ -48,6 +48,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri Mar 18 14:31:50 2005 +0100 @@ -116,11 +116,15 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline +\isanewline +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Mar 18 14:31:50 2005 +0100 @@ -152,9 +152,11 @@ \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -182,9 +184,11 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -213,17 +217,21 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline +\isamarkupfalse% +\isamarkupfalse% \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Fri Mar 18 14:31:50 2005 +0100 @@ -59,7 +59,6 @@ \isamarkupfalse% \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse% % @@ -134,7 +133,6 @@ \isanewline \isanewline \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline \isamarkupfalse% @@ -196,7 +194,6 @@ \isamarkupfalse% \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline \isamarkupfalse% @@ -205,7 +202,6 @@ \isamarkupfalse% \isanewline \isanewline -\isanewline \isamarkupfalse% \isacommand{end}\isanewline \isanewline diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Fri Mar 18 14:31:50 2005 +0100 @@ -103,12 +103,10 @@ \isamarkupfalse% \isanewline \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{end}\isanewline \isanewline diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Fri Mar 18 14:31:50 2005 +0100 @@ -48,6 +48,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri Mar 18 14:31:50 2005 +0100 @@ -115,7 +115,6 @@ \isamarkupfalse% \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline \isamarkupfalse% @@ -150,6 +149,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Fri Mar 18 14:31:50 2005 +0100 @@ -74,6 +74,7 @@ \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse% +\isanewline \isamarkupfalse% % \begin{isamarkuptext}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Misc/document/Plus.tex --- a/doc-src/TutorialI/Misc/document/Plus.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Misc/document/Plus.tex Fri Mar 18 14:31:50 2005 +0100 @@ -19,8 +19,10 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Fri Mar 18 14:31:50 2005 +0100 @@ -20,6 +20,7 @@ \isamarkuptrue% \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -32,6 +33,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Fri Mar 18 14:31:50 2005 +0100 @@ -20,8 +20,10 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Mar 18 14:31:50 2005 +0100 @@ -265,6 +265,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse% +\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -297,6 +298,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -321,6 +323,7 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -347,6 +350,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% % \isamarkupsubsection{Tracing% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Fri Mar 18 14:31:50 2005 +0100 @@ -5,6 +5,7 @@ \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% % diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Mar 18 14:31:50 2005 +0100 @@ -96,7 +96,6 @@ \isamarkupfalse% \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Mar 18 14:31:50 2005 +0100 @@ -141,6 +141,7 @@ \isamarkuptrue% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% % \isamarkupsubsubsection{First Lemma% @@ -159,6 +160,7 @@ \isamarkuptrue% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% % \isamarkupsubsubsection{Second Lemma% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Fri Mar 18 14:31:50 2005 +0100 @@ -158,16 +158,28 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline +\isanewline +\isanewline +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline +\isanewline +\isanewline +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -176,16 +188,14 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Fri Mar 18 14:31:50 2005 +0100 @@ -15,7 +15,6 @@ \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isamarkupfalse% \isamarkuptrue% \isanewline -\isanewline \isamarkupfalse% \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isamarkupfalse% @@ -101,7 +100,6 @@ \isamarkupfalse% \isanewline \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% @@ -229,7 +227,6 @@ \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% @@ -315,14 +312,12 @@ \isamarkupfalse% \isamarkuptrue% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isamarkupfalse% \isamarkuptrue% \isamarkupfalse% \isamarkuptrue% \isanewline -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Types/document/Overloading2.tex --- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Fri Mar 18 14:31:50 2005 +0100 @@ -13,7 +13,6 @@ \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline \isamarkupfalse% \isanewline -\isanewline \isamarkupfalse% \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Thu Mar 17 15:12:03 2005 +0100 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Mar 18 14:31:50 2005 +0100 @@ -92,6 +92,7 @@ \isamarkupfalse% \isamarkupfalse% \isamarkuptrue% +\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse%