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/Library/Quotient_List.thy
changeset 36812 e090bdb4e1c5
parent 36276 92011cc923f5
child 37492 ab36b1a50ca8 
--- a/src/HOL/Library/Quotient_List.thy	Mon May 10 14:53:33 2010 -0700
+++ b/src/HOL/Library/Quotient_List.thy	Tue May 11 07:45:47 2010 +0100
@@ -52,12 +52,17 @@
 lemma list_rel_transp:
   assumes a: "equivp R"
   shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
-  apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
-  apply(simp_all)
+  using a
+  apply(induct R xs1 xs2 arbitrary: xs3 rule: list_rel.induct)
+  apply(simp)
+  apply(simp)
+  apply(simp)
   apply(case_tac xs3)
-  apply(simp_all)
-  apply(rule equivp_transp[OF a])
-  apply(auto)
+  apply(clarify)
+  apply(simp (no_asm_use))
+  apply(clarify)
+  apply(simp (no_asm_use))
+  apply(auto intro: equivp_transp)
   done
 
 lemma list_equivp[quot_equiv]:
isabelle