src/HOL/Induct/Acc.thy
changeset 9906 5c027cca6262
parent 9802 adda1dc18bb8
child 9941 fe05af7ec816
     1.1 --- a/src/HOL/Induct/Acc.thy	Thu Sep 07 21:06:55 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Thu Sep 07 21:10:11 2000 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  inductive "acc r"
     1.6    intros
     1.7 -    accI [rulify_prems]:
     1.8 +    accI [rulified]:
     1.9        "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    1.10  
    1.11  syntax