| changeset 90 | 5c7a69cef18b |
| parent 76 | fb4fe9f8c3cd |
| child 171 | 16c4ea954511 |
--- a/equalities.ML Fri Jun 24 15:11:39 1994 +0200 +++ b/equalities.ML Wed Jun 29 12:04:04 1994 +0200 @@ -307,7 +307,7 @@ by (fast_tac eq_cs 1); val Diff_partition = result(); -goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set"; +goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)"; by (fast_tac eq_cs 1); val double_diff = result();