--- 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"
--- 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
--- 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]