equal
deleted
inserted
replaced
275 goal Set.thy "Inter(insert a B) = a Int Inter(B)"; |
275 goal Set.thy "Inter(insert a B) = a Int Inter(B)"; |
276 by (fast_tac eq_cs 1); |
276 by (fast_tac eq_cs 1); |
277 qed "Inter_insert"; |
277 qed "Inter_insert"; |
278 Addsimps[Inter_insert]; |
278 Addsimps[Inter_insert]; |
279 |
279 |
280 (* Why does fast_tac fail??? |
280 goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)"; |
281 goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)"; |
281 by (fast_tac set_cs 1); |
282 by (fast_tac eq_cs 1); |
282 qed "Inter_Un_subset"; |
283 qed "Inter_Int_distrib"; |
|
284 Addsimps[Inter_Int_distrib]; |
|
285 *) |
|
286 |
283 |
287 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; |
284 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; |
288 by (best_tac eq_cs 1); |
285 by (best_tac eq_cs 1); |
289 qed "Inter_Un_distrib"; |
286 qed "Inter_Un_distrib"; |
290 |
287 |