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