# HG changeset patch
# User nipkow
# Date 1030901965 -7200
# Node ID 83d674e8cd2a63c5b1d0ac1b9c98f75a1b4829f8
# Parent  b7f64ee8da84b5b0250c7cb2438aa72b5a9fbe71
*** empty log message ***

diff -r b7f64ee8da84 -r 83d674e8cd2a doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Sat Aug 31 14:03:49 2002 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Sun Sep 01 19:39:25 2002 +0200
@@ -281,7 +281,7 @@
 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.
 *};
 (*<*)
-lemma infinity_lemma:
+lemma
 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>
  \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
 apply(subgoal_tac