
diff -r 45b8ddc2fab8 -r 85b684d3fdbd doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Sat Mar 18 18:33:40 2006 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Sat Mar 18 18:33:49 2006 +0100
@@ -114,7 +114,7 @@
 \ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}%
 \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}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymle}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}%
 \end{isabelle}
 
 \noindent




