--- a/src/HOL/Library/Quotient_Option.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Mon Sep 13 11:13:15 2010 +0200
@@ -66,16 +66,16 @@
lemma option_Some_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> Option.map Abs) Some = Some"
- apply(simp add: ext_iff)
+ apply(simp add: fun_eq_iff)
apply(simp add: Quotient_abs_rep[OF q])
done
lemma option_map_id[id_simps]:
shows "Option.map id = id"
- by (simp add: ext_iff split_option_all)
+ by (simp add: fun_eq_iff split_option_all)
lemma option_rel_eq[id_simps]:
shows "option_rel (op =) = (op =)"
- by (simp add: ext_iff split_option_all)
+ by (simp add: fun_eq_iff split_option_all)
end