Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transitive_Closure.thy
changeset 35216 7641e8d831d2
parent 34970 4c316d777461
child 37391 476270a6c2dc 
--- a/src/HOL/Transitive_Closure.thy	Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 18 14:21:44 2010 -0800
@@ -464,7 +464,7 @@
    apply (rule subsetI)
    apply (simp only: split_tupled_all)
    apply (erule trancl_induct, blast)
-   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
+   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   apply (rule subsetI)
   apply (blast intro: trancl_mono rtrancl_mono
     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
@@ -503,7 +503,7 @@
   apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
    apply (rule cases)
    apply (erule conversepD)
-  apply (blast intro: prems dest!: tranclp_converseD conversepD)
+  apply (blast intro: assms dest!: tranclp_converseD)
   done
 
 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
isabelle