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

--- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Jun 27 17:51:28 2011 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Jun 27 22:20:49 2011 +0200
@@ -15,6 +15,19 @@
 %
 \endisadelimtheory
 %
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
 \begin{isamarkuptext}%
 The premises of introduction rules may contain universal quantifiers and
 monotone functions.  A universal quantifier lets the rule