| changeset 1917 | 27b71d839d50 |
| parent 1884 | 5a1f81da3e12 |
| child 2021 | dd5866263153 |
--- a/src/HOL/equalities.ML Mon Aug 19 11:23:25 1996 +0200 +++ b/src/HOL/equalities.ML Mon Aug 19 11:25:04 1996 +0200 @@ -211,6 +211,10 @@ by (Fast_tac 1); qed "Un_insert_left"; +goal Set.thy "A Un (insert a B) = insert a (A Un B)"; +by (Fast_tac 1); +qed "Un_insert_right"; + goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; by (Fast_tac 1); qed "Un_Int_distrib";