# 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 "\ Q s; \ s. Q s \ (\ t. (s,t)\M \ Q t) \ \ \ p\Paths s. \ i. Q(p i)"; apply(subgoal_tac