Added macro `termi'
authornipkow
Thu Aug 06 12:46:38 1998 +0200 (1998-08-06)
changeset 527370f478d55606
parent 5272 95cfd872fe66
child 5274 5a29c309b0b7
Added macro `termi'
src/HOL/Induct/Acc.thy
     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