1.1 --- a/doc-src/TutorialI/Overview/Isar.thy	Wed Jun 26 10:26:46 2002 +0200
     1.2 +++ b/doc-src/TutorialI/Overview/Isar.thy	Wed Jun 26 11:07:14 2002 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  proof
     1.5    show "lfp ?F \<subseteq> ?toA"
     1.6    by (blast intro!: lfp_lowerbound intro: rtrancl_trans)
     1.7 -
     1.8 +next
     1.9    show "?toA \<subseteq> lfp ?F"
    1.10    proof
    1.11      fix s assume "s \<in> ?toA"
    1.12 @@ -20,6 +20,7 @@
    1.13      proof (rule converse_rtrancl_induct)
    1.14        from tA have "t \<in> ?F (lfp ?F)" by blast
    1.15        with mono_ef show "t \<in> lfp ?F" ..
    1.16 +    next
    1.17        fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*"
    1.18                    and "s' \<in> lfp ?F"
    1.19        then have "s \<in> ?F (lfp ?F)" by blast