Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Tue, 11 May 2010 08:52:22 +0100
changeset 36813 75d837441aa6
parent 36812 e090bdb4e1c5 (diff)
parent 36811 4ab4aa5bee1c (current diff)
child 36815 fc672bf92fc2
child 36831 3037d6810fca
child 36844 5f9385ecc1a7
merged
src/HOL/Tools/Qelim/cooper_data.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/generated_cooper.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Quotient_List.thy	Tue May 11 08:36:02 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Tue May 11 08:52:22 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