src/HOL/Set.ML
changeset 2024 909153d8318f
parent 1985 84cf16192e03
child 2031 03a843f0f447
     1.1 --- a/src/HOL/Set.ML	Wed Sep 25 11:10:31 1996 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Sep 25 11:14:18 1996 +0200
     1.3 @@ -501,8 +501,8 @@
     1.4  (*** Set reasoning tools ***)
     1.5  
     1.6  
     1.7 -val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
     1.8 -		  mem_Collect_eq];
     1.9 +val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.10 +		 mem_Collect_eq];
    1.11  
    1.12  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.13  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";