# HG changeset patch
# User berghofe
# Date 1162895305 -3600
# Node ID 6649bf75b9dc5b02c4d368dbaf5666466ebf5366
# Parent  803bc7672d17aa93c1766f8e7374254f7a844f55
Adapted to changes in FixedPoint theory.

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);*)