src/HOL/Transitive_Closure.thy
changeset 35216 7641e8d831d2
parent 34970 4c316d777461
child 37391 476270a6c2dc
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -464,7 +464,7 @@
     1.4     apply (rule subsetI)
     1.5     apply (simp only: split_tupled_all)
     1.6     apply (erule trancl_induct, blast)
     1.7 -   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
     1.8 +   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
     1.9    apply (rule subsetI)
    1.10    apply (blast intro: trancl_mono rtrancl_mono
    1.11      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
    1.12 @@ -503,7 +503,7 @@
    1.13    apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
    1.14     apply (rule cases)
    1.15     apply (erule conversepD)
    1.16 -  apply (blast intro: prems dest!: tranclp_converseD conversepD)
    1.17 +  apply (blast intro: assms dest!: tranclp_converseD)
    1.18    done
    1.19  
    1.20  lemmas converse_trancl_induct = converse_tranclp_induct [to_set]