equal
deleted
inserted
replaced
209 |
209 |
210 goal Set.thy "(insert a B) Un C = insert a (B Un C)"; |
210 goal Set.thy "(insert a B) Un C = insert a (B Un C)"; |
211 by (Fast_tac 1); |
211 by (Fast_tac 1); |
212 qed "Un_insert_left"; |
212 qed "Un_insert_left"; |
213 |
213 |
|
214 goal Set.thy "A Un (insert a B) = insert a (A Un B)"; |
|
215 by (Fast_tac 1); |
|
216 qed "Un_insert_right"; |
|
217 |
214 goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
218 goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; |
215 by (Fast_tac 1); |
219 by (Fast_tac 1); |
216 qed "Un_Int_distrib"; |
220 qed "Un_Int_distrib"; |
217 |
221 |
218 goal Set.thy |
222 goal Set.thy |