# HG changeset patch
# User haftmann
# Date 1324738390 -3600
# Node ID 562e99c3d3166d364f8819918184a1ced315db46
# Parent  e8fa5090fa04b8b34153311d4ca1400a396f0150
dropped references to obsolete fact `mem_def`

diff -r e8fa5090fa04 -r 562e99c3d316 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -364,7 +364,7 @@
 
 lemma part_equivpI:
   "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
-  by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE)
+  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)
 
 lemma part_equivpE:
   assumes "part_equivp R"
@@ -413,7 +413,7 @@
 
 lemma equivpI:
   "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
-  by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
+  by (auto elim: reflpE sympE transpE simp add: equivp_def)
 
 lemma equivpE:
   assumes "equivp R"
diff -r e8fa5090fa04 -r 562e99c3d316 src/HOL/Library/List_Cset.thy
--- a/src/HOL/Library/List_Cset.thy	Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Library/List_Cset.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -125,7 +125,7 @@
   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
 
 instance proof
-qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def)
+qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff)
 
 end
 
diff -r e8fa5090fa04 -r 562e99c3d316 src/HOL/TPTP/CASC_Setup.thy
--- a/src/HOL/TPTP/CASC_Setup.thy	Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/TPTP/CASC_Setup.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -89,8 +89,6 @@
 lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
 by (metis injI of_rat_eq_iff rat_to_real_def)
 
-declare mem_def [simp add]
-
 declare [[smt_oracle]]
 
 refute_params [maxtime = 10000, no_assms, expect = genuine]