doc-src/TutorialI/CTL/CTL.thy
changeset 21260 11ba04d15f36
parent 18724 cb6e0064c88c
child 27015 f8537d69f514
--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Nov 09 11:58:13 2006 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Nov 09 11:58:43 2006 +0100
@@ -87,7 +87,7 @@
 apply(rule equalityI);
  apply(rule subsetI);
  apply(simp);
- apply(erule lfp_induct);
+ apply(erule lfp_induct_set);
   apply(rule mono_ef);
  apply(simp);
  apply(blast intro: rtrancl_trans);