# HG changeset patch
# User wenzelm
# Date 1163069923 -3600
# Node ID 11ba04d15f36d6202f9a901e96446fae87a2d6eb
# Parent  63ab016c99ca461559b17fc5983b91903d7eae53
lfp_induct_set;

diff -r 63ab016c99ca -r 11ba04d15f36 doc-src/TutorialI/CTL/CTL.thy
--- 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);