# HG changeset patch # User lcp # Date 763909688 -3600 # Node ID 2e9a86203d5977f7ec62ef88a70ace3dfb8414a6 # Parent 9f35f2744fa8c54e07de209e50e9c0c5e1dfc8ae HOL/equalities/Int_Union_image, Un_Inter_image: renamed Int_Union, Un_Inter as they do not refer to images. diff -r 9f35f2744fa8 -r 2e9a86203d59 equalities.ML --- 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);