# HG changeset patch
# User wenzelm
# Date 936363235 -7200
# Node ID 18df569537924c62207ceffbef3d7e3081d05152
# Parent  c2289eabf706bedb4d71427dd838c828c4a43795
no_qed;

diff -r c2289eabf706 -r 18df56953792 src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Fri Sep 03 14:52:19 1999 +0200
+++ b/src/HOL/Induct/Acc.ML	Fri Sep 03 14:53:55 1999 +0200
@@ -27,6 +27,8 @@
 by (Blast_tac 1);
  by (blast_tac (claset() addDs [acc_downward]) 1);
 val lemma = result();
+no_qed();
+
 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
 by (blast_tac (claset() addDs [lemma]) 1);
 qed "acc_downwards";