src/HOL/Induct/Acc.thy
changeset 9596 6d6bf351b2cc
parent 9101 b643f4d7b9e9
child 9802 adda1dc18bb8
     1.1 --- a/src/HOL/Induct/Acc.thy	Mon Aug 14 18:08:26 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Mon Aug 14 18:13:14 2000 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
     1.5  
     1.6  inductive "acc r"
     1.7 -  intrs
     1.8 +  intros
     1.9      accI [rulify_prems]:
    1.10        "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.11