Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
authorpaulson
Tue Jul 01 10:37:03 1997 +0200 (1997-07-01)
changeset 346961d927bd57ec
parent 3468 1f972dc8eafb
child 3470 8160cc3f6d40
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Tue Jul 01 10:34:30 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Jul 01 10:37:03 1997 +0200
     1.3 @@ -10,7 +10,8 @@
     1.4  
     1.5  section "Relating predicates and sets";
     1.6  
     1.7 -AddIffs [mem_Collect_eq];
     1.8 +Addsimps [Collect_mem_eq];
     1.9 +AddIffs  [mem_Collect_eq];
    1.10  
    1.11  goal Set.thy "!!a. P(a) ==> a : {x.P(x)}";
    1.12  by (Asm_simp_tac 1);