--- a/src/ZF/Sum.ML Tue Mar 26 11:45:54 1996 +0100
+++ b/src/ZF/Sum.ML Tue Mar 26 11:50:40 1996 +0100
@@ -115,6 +115,10 @@
by (fast_tac ZF_cs 1);
qed "sum_equal_iff";
+goalw Sum.thy [sum_def] "A+A = 2*A";
+by (fast_tac eq_cs 1);
+qed "sum_eq_2_times";
+
(*** Eliminator -- case ***)