diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Predicate.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -72,7 +72,7 @@
   by (simp add: mem_def)
 
 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
-  by (simp add: expand_fun_eq mem_def)
+  by (simp add: ext_iff mem_def)
 
 
 subsubsection {* Order relation *}
@@ -99,10 +99,10 @@
   by (simp add: bot_fun_eq bot_bool_eq)
 
 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 
 subsubsection {* Binary union *}
@@ -197,10 +197,10 @@
   by (auto simp add: SUP2_iff)
 
 lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
-  by (simp add: SUP1_iff expand_fun_eq)
+  by (simp add: SUP1_iff ext_iff)
 
 lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
-  by (simp add: SUP2_iff expand_fun_eq)
+  by (simp add: SUP2_iff ext_iff)
 
 
 subsubsection {* Intersections of families *}
@@ -230,10 +230,10 @@
   by (auto simp add: INF2_iff)
 
 lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
-  by (simp add: INF1_iff expand_fun_eq)
+  by (simp add: INF1_iff ext_iff)
 
 lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
-  by (simp add: INF2_iff expand_fun_eq)
+  by (simp add: INF2_iff ext_iff)
 
 
 subsection {* Predicates as relations *}
@@ -251,7 +251,7 @@
 
 lemma pred_comp_rel_comp_eq [pred_set_conv]:
   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
-  by (auto simp add: expand_fun_eq elim: pred_compE)
+  by (auto simp add: ext_iff elim: pred_compE)
 
 
 subsubsection {* Converse *}
@@ -276,7 +276,7 @@
 
 lemma conversep_converse_eq [pred_set_conv]:
   "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   by (iprover intro: order_antisym conversepI dest: conversepD)
@@ -294,10 +294,10 @@
     (iprover intro: conversepI ext dest: conversepD)
 
 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 lemma conversep_eq [simp]: "(op =)^--1 = op ="
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 
 subsubsection {* Domain *}
@@ -347,7 +347,7 @@
   "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
 
 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
-  by (auto simp add: Powp_def expand_fun_eq)
+  by (auto simp add: Powp_def ext_iff)
 
 lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
 
@@ -430,7 +430,7 @@
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (auto simp add: bind_def expand_fun_eq)
+  by (auto simp add: bind_def ext_iff)
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
@@ -442,14 +442,14 @@
 
 lemma bottom_bind:
   "\<bottom> \<guillemotright>= P = \<bottom>"
-  by (auto simp add: bot_pred_def bind_def expand_fun_eq)
+  by (auto simp add: bot_pred_def bind_def ext_iff)
 
 lemma sup_bind:
   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
-  by (auto simp add: bind_def sup_pred_def expand_fun_eq)
+  by (auto simp add: bind_def sup_pred_def ext_iff)
 
 lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
+  by (auto simp add: bind_def Sup_pred_def SUP1_iff ext_iff)
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -457,7 +457,7 @@
   shows "A = B"
 proof -
   from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
-  then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq)
+  then show ?thesis by (cases A, cases B) (simp add: ext_iff)
 qed
   
 lemma singleI: "eval (single x) x"
@@ -492,7 +492,7 @@
 
 lemma single_not_bot [simp]:
   "single x \<noteq> \<bottom>"
-  by (auto simp add: single_def bot_pred_def expand_fun_eq)
+  by (auto simp add: single_def bot_pred_def ext_iff)
 
 lemma not_bot:
   assumes "A \<noteq> \<bottom>"
@@ -512,7 +512,7 @@
 
 lemma not_is_empty_single:
   "\<not> is_empty (single x)"
-  by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
+  by (auto simp add: is_empty_def single_def bot_pred_def ext_iff)
 
 lemma is_empty_sup:
   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
@@ -543,7 +543,7 @@
   moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
     by (rule singleton_eqI)
   ultimately have "eval (single (singleton dfault A)) = eval A"
-    by (simp (no_asm_use) add: single_def expand_fun_eq) blast
+    by (simp (no_asm_use) add: single_def ext_iff) blast
   then show ?thesis by (simp add: eval_inject)
 qed
 
@@ -714,13 +714,13 @@
   "member xq = eval (pred_of_seq xq)"
 proof (induct xq)
   case Empty show ?case
-  by (auto simp add: expand_fun_eq elim: botE)
+  by (auto simp add: ext_iff elim: botE)
 next
   case Insert show ?case
-  by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI)
+  by (auto simp add: ext_iff elim: supE singleE intro: supI1 supI2 singleI)
 next
   case Join then show ?case
-  by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2)
+  by (auto simp add: ext_iff elim: supE intro: supI1 supI2)
 qed
 
 lemma eval_code [code]: "eval (Seq f) = member (f ())"