# HG changeset patch
# User wenzelm
# Date 931531495 -7200
# Node ID 214e41d27d74e13f43325075520ddfa13ecd2c6e
# Parent  2cde117d2738da743d952e73fb140b9e67668056
removed qed_with;

diff -r 2cde117d2738 -r 214e41d27d74 src/HOL/Isar_examples/NatSum.thy
--- a/src/HOL/Isar_examples/NatSum.thy	Fri Jul 09 10:49:14 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Fri Jul 09 16:44:55 1999 +0200
@@ -33,13 +33,13 @@
   qed "sum_of_naturals";
 *)
 
-theorem "2 * sum (%i. i) (Suc n) = n * Suc n";
+theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
 proof same;
   apply simp_tac;
   apply (induct n);
   apply simp_tac;
   apply asm_simp_tac;
-qed_with sum_of_naturals;
+qed;
 
 
 text {* Proper Isabelle/Isar proof expressing the same reasoning (which