equal
deleted
inserted
replaced
305 |
305 |
306 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B"; |
306 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B"; |
307 by (fast_tac eq_cs 1); |
307 by (fast_tac eq_cs 1); |
308 val Diff_partition = result(); |
308 val Diff_partition = result(); |
309 |
309 |
310 goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set"; |
310 goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)"; |
311 by (fast_tac eq_cs 1); |
311 by (fast_tac eq_cs 1); |
312 val double_diff = result(); |
312 val double_diff = result(); |
313 |
313 |
314 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)"; |
314 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)"; |
315 by (fast_tac eq_cs 1); |
315 by (fast_tac eq_cs 1); |