| changeset 9312 | a93a7b6bb654 |
| parent 9206 | eaaee6bd74ba |
| child 9338 | fcf7f29a3447 |
--- a/src/HOL/equalities.ML Thu Jul 13 23:09:25 2000 +0200 +++ b/src/HOL/equalities.ML Thu Jul 13 23:10:12 2000 +0200 @@ -592,8 +592,8 @@ Goal "(UNION A B = {}) = (ALL x:A. B x = {})"; by Auto_tac; -qed "UN_empty"; -AddIffs [UN_empty]; +qed "UN_empty3"; +AddIffs [UN_empty3]; (*Distributive laws...*)