src/HOL/Library/Nat_Infinity.thy
changeset 14691 e1eedc8cad37
parent 14565 c6dc17aab88a
child 14706 71590b7733b7
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat May 01 21:59:12 2004 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat May 01 22:01:57 2004 +0200
     1.3 @@ -21,8 +21,7 @@
     1.4  
     1.5  datatype inat = Fin nat | Infty
     1.6  
     1.7 -instance inat :: ord ..
     1.8 -instance inat :: zero ..
     1.9 +instance inat :: "{ord, zero}" ..
    1.10  
    1.11  consts
    1.12    iSuc :: "inat => inat"