equalities.ML
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();