Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Library/Quotient_List.thy
changeset 36812 e090bdb4e1c5
parent 36276 92011cc923f5
child 37492 ab36b1a50ca8 
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Mon May 10 14:53:33 2010 -0700
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue May 11 07:45:47 2010 +0100
     1.3 @@ -52,12 +52,17 @@
     1.4  lemma list_rel_transp:
     1.5    assumes a: "equivp R"
     1.6    shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
     1.7 -  apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
     1.8 -  apply(simp_all)
     1.9 +  using a
    1.10 +  apply(induct R xs1 xs2 arbitrary: xs3 rule: list_rel.induct)
    1.11 +  apply(simp)
    1.12 +  apply(simp)
    1.13 +  apply(simp)
    1.14    apply(case_tac xs3)
    1.15 -  apply(simp_all)
    1.16 -  apply(rule equivp_transp[OF a])
    1.17 -  apply(auto)
    1.18 +  apply(clarify)
    1.19 +  apply(simp (no_asm_use))
    1.20 +  apply(clarify)
    1.21 +  apply(simp (no_asm_use))
    1.22 +  apply(auto intro: equivp_transp)
    1.23    done
    1.24  
    1.25  lemma list_equivp[quot_equiv]:
isabelle