# HG changeset patch
# User wenzelm
# Date 1134672122 -3600
# Node ID 560f89584ada3ae835a7aabcde265ab9c4b77f33
# Parent  50c0c118e96db6e0ff7e4a3e41a8ed00e40847fc
acc_induct: proper tags;

diff -r 50c0c118e96d -r 560f89584ada src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Thu Dec 15 19:42:00 2005 +0100
+++ b/src/ZF/Induct/Acc.thy	Thu Dec 15 19:42:02 2005 +0100
@@ -35,7 +35,7 @@
 lemma acc_downward: "[| b \<in> acc(r);  <a,b>: r |] ==> a \<in> acc(r)"
   by (erule acc.cases) blast
 
-lemma acc_induct [induct set: acc]:
+lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
     "[| a \<in> acc(r);
         !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
      |] ==> P(a)"