--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Feb 01 18:01:57 2005 +0100
@@ -85,37 +85,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-The proof is by showing that our relation is a subset of another well-founded
-relation: one given by a measure function.\index{*wf_subset (theorem)}%
-\end{isamarkuptxt}%
+\isamarkuptrue%
+\isamarkupfalse%
\isamarkuptrue%
-\isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}%
-\end{isabelle}
-
-\noindent
-The inclusion remains to be proved. After unfolding some definitions,
-we are left with simple arithmetic:%
-\end{isamarkuptxt}%
+\isamarkupfalse%
\isamarkuptrue%
-\isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
-%
-\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:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\ arith\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent