src/HOL/Set.ML

 
 
 (*** Set reasoning tools ***)
 
 
-val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
-		  mem_Collect_eq];
+val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
+		 mem_Collect_eq];
 
 (*Not for Addsimps -- it can cause goals to blow up!*)
 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 qed "mem_if";