doc-src/TutorialI/Advanced/document/WFrec.tex

--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 19:23:04 2006 +0200
@@ -119,22 +119,11 @@
 
 \noindent
 The inclusion remains to be proved. After unfolding some definitions, 
-we are left with simple arithmetic:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
-\end{isabelle}
-
-\noindent
-And that is dispatched automatically:%
+we are left with simple arithmetic that is dispatched automatically.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{by}\isamarkupfalse%
-\ arith%
+\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %