author | wenzelm |
Thu, 15 Dec 2005 19:42:02 +0100 | |
changeset 18414 | 560f89584ada |
parent 18413 | 50c0c118e96d |
child 18415 | eb68dc98bda2 |
--- 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)"