--- a/equalities.ML Thu Mar 17 11:27:29 1994 +0100
+++ b/equalities.ML Thu Mar 17 14:08:08 1994 +0100
@@ -186,7 +186,7 @@
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
by (fast_tac eq_cs 1);
-val Int_Union_image = result();
+val Int_Union = result();
(* Devlin, page 12: Union of a family of unions **)
goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)";
@@ -195,7 +195,7 @@
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
by (fast_tac eq_cs 1);
-val Un_Inter_image = result();
+val Un_Inter = result();
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
by (best_tac eq_cs 1);