src/HOL/Library/Quotient_Sum.thy
changeset 39198 f967a16dfcdd
parent 37678 0040bafffdef
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4    assumes q1: "Quotient R1 Abs1 Rep1"
     1.5    assumes q2: "Quotient R2 Abs2 Rep2"
     1.6    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
     1.7 -  apply(simp add: expand_fun_eq)
     1.8 +  apply(simp add: ext_iff)
     1.9    apply(simp add: Quotient_abs_rep[OF q1])
    1.10    done
    1.11  
    1.12 @@ -82,16 +82,16 @@
    1.13    assumes q1: "Quotient R1 Abs1 Rep1"
    1.14    assumes q2: "Quotient R2 Abs2 Rep2"
    1.15    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    1.16 -  apply(simp add: expand_fun_eq)
    1.17 +  apply(simp add: ext_iff)
    1.18    apply(simp add: Quotient_abs_rep[OF q2])
    1.19    done
    1.20  
    1.21  lemma sum_map_id[id_simps]:
    1.22    shows "sum_map id id = id"
    1.23 -  by (simp add: expand_fun_eq split_sum_all)
    1.24 +  by (simp add: ext_iff split_sum_all)
    1.25  
    1.26  lemma sum_rel_eq[id_simps]:
    1.27    shows "sum_rel (op =) (op =) = (op =)"
    1.28 -  by (simp add: expand_fun_eq split_sum_all)
    1.29 +  by (simp add: ext_iff split_sum_all)
    1.30  
    1.31  end