dropped references to obsolete fact `mem_def`
authorhaftmann
Sat Dec 24 15:53:10 2011 +0100 (2011-12-24)
changeset 45969562e99c3d316
parent 45968 e8fa5090fa04
child 45970 b6d0cff57d96
dropped references to obsolete fact `mem_def`
src/HOL/Equiv_Relations.thy
src/HOL/Library/List_Cset.thy
src/HOL/TPTP/CASC_Setup.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -364,7 +364,7 @@
     1.4  
     1.5  lemma part_equivpI:
     1.6    "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
     1.7 -  by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE)
     1.8 +  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)
     1.9  
    1.10  lemma part_equivpE:
    1.11    assumes "part_equivp R"
    1.12 @@ -413,7 +413,7 @@
    1.13  
    1.14  lemma equivpI:
    1.15    "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
    1.16 -  by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
    1.17 +  by (auto elim: reflpE sympE transpE simp add: equivp_def)
    1.18  
    1.19  lemma equivpE:
    1.20    assumes "equivp R"
     2.1 --- a/src/HOL/Library/List_Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     2.2 +++ b/src/HOL/Library/List_Cset.thy	Sat Dec 24 15:53:10 2011 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4    "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
     2.5  
     2.6  instance proof
     2.7 -qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def)
     2.8 +qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff)
     2.9  
    2.10  end
    2.11  
     3.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Sat Dec 24 15:53:10 2011 +0100
     3.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Sat Dec 24 15:53:10 2011 +0100
     3.3 @@ -89,8 +89,6 @@
     3.4  lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
     3.5  by (metis injI of_rat_eq_iff rat_to_real_def)
     3.6  
     3.7 -declare mem_def [simp add]
     3.8 -
     3.9  declare [[smt_oracle]]
    3.10  
    3.11  refute_params [maxtime = 10000, no_assms, expect = genuine]