src/HOL/Relation_Power.thy
changeset 12338 de0f4a63baa5
parent 11306 6f4ed75b2dca
child 15112 6f0772a94299
     1.1 --- a/src/HOL/Relation_Power.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Relation_Power.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  Relation_Power = Nat +
     1.5  
     1.6  instance
     1.7 -  set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
     1.8 +  set :: (type) power   (* only ('a * 'a) set should be in power! *)
     1.9  
    1.10  primrec (relpow)
    1.11    "R^0 = Id"
    1.12 @@ -23,7 +23,7 @@
    1.13  
    1.14  
    1.15  instance
    1.16 -  fun :: (term,term)power   (* only 'a => 'a should be in power! *)
    1.17 +  fun :: (type, type) power   (* only 'a => 'a should be in power! *)
    1.18  
    1.19  primrec (funpow)
    1.20    "f^0 = id"