src/HOL/Induct/Acc.thy
changeset 7800 8ee919e42174
parent 7759 44dd5dc8e90f
child 7867 2efb66472812
     1.1 --- a/src/HOL/Induct/Acc.thy	Fri Oct 08 15:08:47 1999 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Fri Oct 08 15:09:14 1999 +0200
     1.3 @@ -18,10 +18,12 @@
     1.4  
     1.5  inductive "acc r"
     1.6    intrs
     1.7 -    accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
     1.8 -
     1.9 +    accI [rulify_prems]:
    1.10 +      "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.11  
    1.12 -syntax        termi :: "('a * 'a)set => 'a set"
    1.13 -translations "termi r" == "acc(r^-1)"
    1.14 +syntax
    1.15 +  termi :: "('a * 'a)set => 'a set"
    1.16 +translations
    1.17 +  "termi r" == "acc(r^-1)"
    1.18  
    1.19  end