changeset 2024 | 909153d8318f |
parent 1985 | 84cf16192e03 |
child 2031 | 03a843f0f447 |
--- a/src/HOL/Set.ML Wed Sep 25 11:10:31 1996 +0200 +++ b/src/HOL/Set.ML Wed Sep 25 11:14:18 1996 +0200 @@ -501,8 +501,8 @@ (*** 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))";