src/CCL/set.ML

--- a/src/CCL/set.ML	Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/set.ML	Mon Sep 20 17:02:11 1993 +0200
@@ -22,18 +22,13 @@
 by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
 val CollectD = result();
 
+val CollectE = make_elim CollectD;
+
 val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
 by (rtac (set_extension RS iffD2) 1);
 by (rtac (prem RS allI) 1);
 val set_ext = result();
 
-val prems = goal Set.thy "[| !!x. P(x) <-> Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
-by (REPEAT (ares_tac [set_ext,iffI,CollectI] 1 ORELSE
-            eresolve_tac ([CollectD] RL (prems RL [iffD1,iffD2])) 1));
-val Collect_cong = result();
-
-val CollectE = make_elim CollectD;
-
 (*** Bounded quantifiers ***)
 
 val prems = goalw Set.thy [Ball_def]