src/HOL/Library/Quotient_Sum.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 40465 2989f9f3aa10
--- a/src/HOL/Library/Quotient_Sum.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -74,7 +74,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
-  apply(simp add: ext_iff)
+  apply(simp add: fun_eq_iff)
   apply(simp add: Quotient_abs_rep[OF q1])
   done
 
@@ -82,16 +82,16 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
-  apply(simp add: ext_iff)
+  apply(simp add: fun_eq_iff)
   apply(simp add: Quotient_abs_rep[OF q2])
   done
 
 lemma sum_map_id[id_simps]:
   shows "sum_map id id = id"
-  by (simp add: ext_iff split_sum_all)
+  by (simp add: fun_eq_iff split_sum_all)
 
 lemma sum_rel_eq[id_simps]:
   shows "sum_rel (op =) (op =) = (op =)"
-  by (simp add: ext_iff split_sum_all)
+  by (simp add: fun_eq_iff split_sum_all)
 
 end