--- 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}%
--- 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}%
--- 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}%
--- 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%
--- 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
--- 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
--- 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
--- 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}%
--- 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}%
--- 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}%
--- 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}%
--- 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}%
--- 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}%
--- 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%
--- 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%
%
--- 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%
--- 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%
--- 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}%
--- 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%
--- 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
--- 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%