diff -r 60ab5844fe81 -r 35e0fd1b1775 src/ZF/Sum.ML
--- 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 ***)