src/HOL/Induct/Acc.thy
changeset 5273 70f478d55606
parent 5102 8c782c25a11e
child 5717 0d28dbe484b6
     1.1 --- a/src/HOL/Induct/Acc.thy	Thu Aug 06 12:46:18 1998 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Thu Aug 06 12:46:38 1998 +0200
     1.3 @@ -23,4 +23,7 @@
     1.4      pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
     1.5    monos     "[Pow_mono]"
     1.6  
     1.7 +syntax        termi :: "('a * 'a)set => 'a set"
     1.8 +translations "termi r" == "acc(r^-1)"
     1.9 +
    1.10  end