--- a/src/HOL/equalities.ML Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/equalities.ML Wed Oct 03 20:54:16 2001 +0200
@@ -888,7 +888,7 @@
by (Blast_tac 1);
qed "set_eq_subset";
-Goal "A <= B = (ALL t. t:A --> t:B)";
+Goal "(A <= B) = (ALL t. t:A --> t:B)";
by (Blast_tac 1);
qed "subset_iff";