diff -r 803bc7672d17 -r 6649bf75b9dc doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Tue Nov 07 09:59:43 2006 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Tue Nov 07 11:28:25 2006 +0100
@@ -102,7 +102,7 @@
 which is proved by @{term lfp}-induction:
 *}
 
- apply(erule lfp_induct)
+ apply(erule lfp_induct_set)
   apply(rule mono_ef)
  apply(simp)
 (*pr(latex xsymbols symbols);*)