# HG changeset patch
# User paulson
# Date 867746223 -7200
# Node ID 61d927bd57ec89099d4e621cacc832c48cdc32b6
# Parent  1f972dc8eafb277175161d06a82bbe6d6cf9ff24
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?

diff -r 1f972dc8eafb -r 61d927bd57ec src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Jul 01 10:34:30 1997 +0200
+++ b/src/HOL/Set.ML	Tue Jul 01 10:37:03 1997 +0200
@@ -10,7 +10,8 @@
 
 section "Relating predicates and sets";
 
-AddIffs [mem_Collect_eq];
+Addsimps [Collect_mem_eq];
+AddIffs  [mem_Collect_eq];
 
 goal Set.thy "!!a. P(a) ==> a : {x.P(x)}";
 by (Asm_simp_tac 1);