auto update
authorpaulson
Fri Mar 18 14:31:50 2005 +0100 (2005-03-18 ago)
changeset 15614b098158a3f39
parent 15613 ab90e95ae02e
child 15615 d72b1867d09d
auto update
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Inductive/document/Even.tex
doc-src/TutorialI/Inductive/document/Mutual.tex
doc-src/TutorialI/Inductive/document/Star.tex
doc-src/TutorialI/Misc/document/Itrev.tex
doc-src/TutorialI/Misc/document/Plus.tex
doc-src/TutorialI/Misc/document/Tree.tex
doc-src/TutorialI/Misc/document/Tree2.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Recdef/document/Nested2.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/document/Pairs.tex
     1.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Thu Mar 17 15:12:03 2005 +0100
     1.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Fri Mar 18 14:31:50 2005 +0100
     1.3 @@ -137,6 +137,7 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  \isamarkupfalse%
     1.7 +\isanewline
     1.8  \isamarkupfalse%
     1.9  \isamarkupfalse%
    1.10  \end{isabellebody}%
     2.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Thu Mar 17 15:12:03 2005 +0100
     2.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Mar 18 14:31:50 2005 +0100
     2.3 @@ -135,12 +135,14 @@
     2.4  \isamarkupfalse%
     2.5  \isamarkupfalse%
     2.6  \isamarkupfalse%
     2.7 +\isanewline
     2.8  \isamarkupfalse%
     2.9  \isamarkupfalse%
    2.10  \isamarkupfalse%
    2.11  \isamarkupfalse%
    2.12  \isamarkupfalse%
    2.13  \isamarkupfalse%
    2.14 +\isanewline
    2.15  \isamarkupfalse%
    2.16  \isamarkupfalse%
    2.17  \end{isabellebody}%
     3.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Thu Mar 17 15:12:03 2005 +0100
     3.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Mar 18 14:31:50 2005 +0100
     3.3 @@ -48,6 +48,7 @@
     3.4  \isamarkupfalse%
     3.5  \isamarkupfalse%
     3.6  \isamarkuptrue%
     3.7 +\isanewline
     3.8  \isamarkupfalse%
     3.9  \isamarkupfalse%
    3.10  \end{isabellebody}%
     4.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Thu Mar 17 15:12:03 2005 +0100
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Mar 18 14:31:50 2005 +0100
     4.3 @@ -116,11 +116,15 @@
     4.4  \isamarkupfalse%
     4.5  \isamarkupfalse%
     4.6  \isamarkupfalse%
     4.7 +\isanewline
     4.8 +\isanewline
     4.9 +\isanewline
    4.10  \isamarkupfalse%
    4.11  \isamarkupfalse%
    4.12  \isamarkupfalse%
    4.13  \isamarkupfalse%
    4.14  \isamarkupfalse%
    4.15 +\isanewline
    4.16  \isamarkupfalse%
    4.17  \isamarkupfalse%
    4.18  \isamarkupfalse%
     5.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Mar 17 15:12:03 2005 +0100
     5.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Mar 18 14:31:50 2005 +0100
     5.3 @@ -152,9 +152,11 @@
     5.4  \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
     5.5  \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse%
     5.6  \isamarkupfalse%
     5.7 +\isanewline
     5.8  \isamarkupfalse%
     5.9  \isamarkupfalse%
    5.10  \isamarkupfalse%
    5.11 +\isanewline
    5.12  \isamarkupfalse%
    5.13  %
    5.14  \begin{isamarkuptext}%
    5.15 @@ -182,9 +184,11 @@
    5.16  \isamarkuptrue%
    5.17  \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%
    5.18  \isamarkupfalse%
    5.19 +\isanewline
    5.20  \isamarkupfalse%
    5.21  \isamarkupfalse%
    5.22  \isamarkupfalse%
    5.23 +\isanewline
    5.24  \isamarkupfalse%
    5.25  %
    5.26  \begin{isamarkuptext}%
    5.27 @@ -213,17 +217,21 @@
    5.28  \isamarkupfalse%
    5.29  \isamarkupfalse%
    5.30  \isamarkupfalse%
    5.31 -\isamarkupfalse%
    5.32 -\isamarkupfalse%
    5.33 +\isanewline
    5.34  \isamarkupfalse%
    5.35  \isamarkupfalse%
    5.36  \isamarkupfalse%
    5.37 +\isanewline
    5.38  \isamarkupfalse%
    5.39  \isamarkupfalse%
    5.40  \isamarkupfalse%
    5.41 +\isanewline
    5.42  \isamarkupfalse%
    5.43  \isamarkupfalse%
    5.44  \isamarkupfalse%
    5.45 +\isanewline
    5.46 +\isamarkupfalse%
    5.47 +\isamarkupfalse%
    5.48  \end{isabellebody}%
    5.49  %%% Local Variables:
    5.50  %%% mode: latex
     6.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Thu Mar 17 15:12:03 2005 +0100
     6.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Fri Mar 18 14:31:50 2005 +0100
     6.3 @@ -59,7 +59,6 @@
     6.4  \isamarkupfalse%
     6.5  \isamarkupfalse%
     6.6  \isanewline
     6.7 -\isanewline
     6.8  \isamarkupfalse%
     6.9  \isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse%
    6.10  %
    6.11 @@ -134,7 +133,6 @@
    6.12  \isanewline
    6.13  \isanewline
    6.14  \isanewline
    6.15 -\isanewline
    6.16  \isamarkupfalse%
    6.17  \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
    6.18  \isamarkupfalse%
    6.19 @@ -196,7 +194,6 @@
    6.20  \isamarkupfalse%
    6.21  \isamarkupfalse%
    6.22  \isanewline
    6.23 -\isanewline
    6.24  \isamarkupfalse%
    6.25  \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
    6.26  \isamarkupfalse%
    6.27 @@ -205,7 +202,6 @@
    6.28  \isamarkupfalse%
    6.29  \isanewline
    6.30  \isanewline
    6.31 -\isanewline
    6.32  \isamarkupfalse%
    6.33  \isacommand{end}\isanewline
    6.34  \isanewline
     7.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Thu Mar 17 15:12:03 2005 +0100
     7.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Fri Mar 18 14:31:50 2005 +0100
     7.3 @@ -103,12 +103,10 @@
     7.4  \isamarkupfalse%
     7.5  \isanewline
     7.6  \isanewline
     7.7 -\isanewline
     7.8  \isamarkupfalse%
     7.9  \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
    7.10  \isamarkupfalse%
    7.11  \isanewline
    7.12 -\isanewline
    7.13  \isamarkupfalse%
    7.14  \isacommand{end}\isanewline
    7.15  \isanewline
     8.1 --- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Thu Mar 17 15:12:03 2005 +0100
     8.2 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Fri Mar 18 14:31:50 2005 +0100
     8.3 @@ -48,6 +48,7 @@
     8.4  \isamarkupfalse%
     8.5  \isamarkupfalse%
     8.6  \isamarkupfalse%
     8.7 +\isanewline
     8.8  \isamarkupfalse%
     8.9  \isamarkupfalse%
    8.10  \end{isabellebody}%
     9.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Thu Mar 17 15:12:03 2005 +0100
     9.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri Mar 18 14:31:50 2005 +0100
     9.3 @@ -115,7 +115,6 @@
     9.4  \isamarkupfalse%
     9.5  \isamarkupfalse%
     9.6  \isanewline
     9.7 -\isanewline
     9.8  \isamarkupfalse%
     9.9  \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
    9.10  \isamarkupfalse%
    9.11 @@ -150,6 +149,7 @@
    9.12  \isamarkupfalse%
    9.13  \isamarkupfalse%
    9.14  \isamarkupfalse%
    9.15 +\isanewline
    9.16  \isamarkupfalse%
    9.17  \isamarkupfalse%
    9.18  \end{isabellebody}%
    10.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Thu Mar 17 15:12:03 2005 +0100
    10.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Mar 18 14:31:50 2005 +0100
    10.3 @@ -74,6 +74,7 @@
    10.4  \isamarkuptrue%
    10.5  \isamarkupfalse%
    10.6  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
    10.7 +\isanewline
    10.8  \isamarkupfalse%
    10.9  %
   10.10  \begin{isamarkuptext}%
    11.1 --- a/doc-src/TutorialI/Misc/document/Plus.tex	Thu Mar 17 15:12:03 2005 +0100
    11.2 +++ b/doc-src/TutorialI/Misc/document/Plus.tex	Fri Mar 18 14:31:50 2005 +0100
    11.3 @@ -19,8 +19,10 @@
    11.4  \isamarkuptrue%
    11.5  \isamarkupfalse%
    11.6  \isamarkupfalse%
    11.7 +\isanewline
    11.8  \isamarkupfalse%
    11.9  \isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
   11.10 +\isanewline
   11.11  \isamarkupfalse%
   11.12  \isamarkupfalse%
   11.13  \end{isabellebody}%
    12.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex	Thu Mar 17 15:12:03 2005 +0100
    12.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex	Fri Mar 18 14:31:50 2005 +0100
    12.3 @@ -20,6 +20,7 @@
    12.4  \isamarkuptrue%
    12.5  \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse%
    12.6  \isamarkupfalse%
    12.7 +\isanewline
    12.8  \isamarkupfalse%
    12.9  \isamarkupfalse%
   12.10  \isamarkupfalse%
   12.11 @@ -32,6 +33,7 @@
   12.12  \isamarkuptrue%
   12.13  \isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
   12.14  \isamarkupfalse%
   12.15 +\isanewline
   12.16  \isamarkupfalse%
   12.17  \isamarkupfalse%
   12.18  \end{isabellebody}%
    13.1 --- a/doc-src/TutorialI/Misc/document/Tree2.tex	Thu Mar 17 15:12:03 2005 +0100
    13.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Fri Mar 18 14:31:50 2005 +0100
    13.3 @@ -20,8 +20,10 @@
    13.4  \isamarkuptrue%
    13.5  \isamarkupfalse%
    13.6  \isamarkupfalse%
    13.7 +\isanewline
    13.8  \isamarkupfalse%
    13.9  \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse%
   13.10 +\isanewline
   13.11  \isamarkupfalse%
   13.12  \isamarkupfalse%
   13.13  \end{isabellebody}%
    14.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Thu Mar 17 15:12:03 2005 +0100
    14.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Mar 18 14:31:50 2005 +0100
    14.3 @@ -265,6 +265,7 @@
    14.4  \end{isamarkuptext}%
    14.5  \isamarkuptrue%
    14.6  \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse%
    14.7 +\isanewline
    14.8  \isamarkupfalse%
    14.9  %
   14.10  \begin{isamarkuptext}%
   14.11 @@ -297,6 +298,7 @@
   14.12  \isamarkupfalse%
   14.13  \isamarkupfalse%
   14.14  \isamarkuptrue%
   14.15 +\isanewline
   14.16  \isamarkupfalse%
   14.17  \isamarkupfalse%
   14.18  \isamarkupfalse%
   14.19 @@ -321,6 +323,7 @@
   14.20  \isamarkuptrue%
   14.21  \isamarkupfalse%
   14.22  \isamarkupfalse%
   14.23 +\isanewline
   14.24  \isamarkupfalse%
   14.25  %
   14.26  \begin{isamarkuptext}%
   14.27 @@ -347,6 +350,7 @@
   14.28  \isamarkupfalse%
   14.29  \isamarkupfalse%
   14.30  \isamarkuptrue%
   14.31 +\isanewline
   14.32  \isamarkupfalse%
   14.33  %
   14.34  \isamarkupsubsection{Tracing%
    15.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Thu Mar 17 15:12:03 2005 +0100
    15.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Fri Mar 18 14:31:50 2005 +0100
    15.3 @@ -5,6 +5,7 @@
    15.4  \isamarkupfalse%
    15.5  \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
    15.6  \isamarkupfalse%
    15.7 +\isanewline
    15.8  \isamarkupfalse%
    15.9  \isamarkupfalse%
   15.10  %
    16.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Thu Mar 17 15:12:03 2005 +0100
    16.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Mar 18 14:31:50 2005 +0100
    16.3 @@ -96,7 +96,6 @@
    16.4  \isamarkupfalse%
    16.5  \isamarkupfalse%
    16.6  \isanewline
    16.7 -\isanewline
    16.8  \isamarkupfalse%
    16.9  \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
   16.10  \isamarkupfalse%
    17.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Mar 17 15:12:03 2005 +0100
    17.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Mar 18 14:31:50 2005 +0100
    17.3 @@ -141,6 +141,7 @@
    17.4  \isamarkuptrue%
    17.5  \isamarkupfalse%
    17.6  \isamarkuptrue%
    17.7 +\isanewline
    17.8  \isamarkupfalse%
    17.9  %
   17.10  \isamarkupsubsubsection{First Lemma%
   17.11 @@ -159,6 +160,7 @@
   17.12  \isamarkuptrue%
   17.13  \isamarkupfalse%
   17.14  \isamarkuptrue%
   17.15 +\isanewline
   17.16  \isamarkupfalse%
   17.17  %
   17.18  \isamarkupsubsubsection{Second Lemma%
    18.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Thu Mar 17 15:12:03 2005 +0100
    18.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Fri Mar 18 14:31:50 2005 +0100
    18.3 @@ -158,16 +158,28 @@
    18.4  \isamarkupfalse%
    18.5  \isamarkupfalse%
    18.6  \isamarkupfalse%
    18.7 +\isanewline
    18.8 +\isanewline
    18.9 +\isanewline
   18.10 +\isanewline
   18.11  \isamarkupfalse%
   18.12  \isamarkupfalse%
   18.13  \isamarkupfalse%
   18.14  \isamarkupfalse%
   18.15  \isamarkupfalse%
   18.16  \isamarkupfalse%
   18.17 +\isanewline
   18.18 +\isamarkupfalse%
   18.19 +\isamarkupfalse%
   18.20  \isamarkupfalse%
   18.21  \isamarkupfalse%
   18.22  \isamarkupfalse%
   18.23  \isamarkupfalse%
   18.24 +\isanewline
   18.25 +\isanewline
   18.26 +\isanewline
   18.27 +\isamarkupfalse%
   18.28 +\isamarkupfalse%
   18.29  \isamarkupfalse%
   18.30  \isamarkupfalse%
   18.31  \isamarkupfalse%
   18.32 @@ -176,16 +188,14 @@
   18.33  \isamarkupfalse%
   18.34  \isamarkupfalse%
   18.35  \isamarkupfalse%
   18.36 +\isanewline
   18.37  \isamarkupfalse%
   18.38  \isamarkupfalse%
   18.39  \isamarkupfalse%
   18.40  \isamarkupfalse%
   18.41  \isamarkupfalse%
   18.42  \isamarkupfalse%
   18.43 -\isamarkupfalse%
   18.44 -\isamarkupfalse%
   18.45 -\isamarkupfalse%
   18.46 -\isamarkupfalse%
   18.47 +\isanewline
   18.48  \isamarkupfalse%
   18.49  \isamarkupfalse%
   18.50  \end{isabellebody}%
    19.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Mar 17 15:12:03 2005 +0100
    19.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Fri Mar 18 14:31:50 2005 +0100
    19.3 @@ -15,7 +15,6 @@
    19.4  \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isamarkupfalse%
    19.5  \isamarkuptrue%
    19.6  \isanewline
    19.7 -\isanewline
    19.8  \isamarkupfalse%
    19.9  \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
   19.10  \isamarkupfalse%
   19.11 @@ -101,7 +100,6 @@
   19.12  \isamarkupfalse%
   19.13  \isanewline
   19.14  \isanewline
   19.15 -\isanewline
   19.16  \isamarkupfalse%
   19.17  \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
   19.18  \isamarkupfalse%
   19.19 @@ -229,7 +227,6 @@
   19.20  \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
   19.21  \isamarkupfalse%
   19.22  \isanewline
   19.23 -\isanewline
   19.24  \isamarkupfalse%
   19.25  \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
   19.26  \isamarkupfalse%
   19.27 @@ -315,14 +312,12 @@
   19.28  \isamarkupfalse%
   19.29  \isamarkuptrue%
   19.30  \isanewline
   19.31 -\isanewline
   19.32  \isamarkupfalse%
   19.33  \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%
   19.34  \isamarkuptrue%
   19.35  \isamarkupfalse%
   19.36  \isamarkuptrue%
   19.37  \isanewline
   19.38 -\isanewline
   19.39  \isamarkupfalse%
   19.40  \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
   19.41  \isamarkupfalse%
    20.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Thu Mar 17 15:12:03 2005 +0100
    20.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Fri Mar 18 14:31:50 2005 +0100
    20.3 @@ -13,7 +13,6 @@
    20.4  \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
    20.5  \isamarkupfalse%
    20.6  \isanewline
    20.7 -\isanewline
    20.8  \isamarkupfalse%
    20.9  \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   20.10  le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
    21.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Thu Mar 17 15:12:03 2005 +0100
    21.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Fri Mar 18 14:31:50 2005 +0100
    21.3 @@ -92,6 +92,7 @@
    21.4  \isamarkupfalse%
    21.5  \isamarkupfalse%
    21.6  \isamarkuptrue%
    21.7 +\isanewline
    21.8  \isamarkupfalse%
    21.9  \isamarkupfalse%
   21.10  \isamarkupfalse%