src/HOL/Integ/Integ.thy
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/Integ/Integ.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Integ/Integ.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -23,13 +23,13 @@
     1.4    int :: {ord, plus, times, minus}
     1.5  
     1.6  consts
     1.7 -  zNat        :: "nat set"
     1.8 -  znat	      :: "nat => int"	   ("$# _" [80] 80)
     1.9 -  zminus      :: "int => int"	   ("$~ _" [80] 80)
    1.10 -  znegative   :: "int => bool"
    1.11 -  zmagnitude  :: "int => int"
    1.12 -  zdiv,zmod   :: "[int,int]=>int"  (infixl 70)
    1.13 -  zpred,zsuc  :: "int=>int"
    1.14 +  zNat        :: nat set
    1.15 +  znat	      :: nat => int	   ("$# _" [80] 80)
    1.16 +  zminus      :: int => int	   ("$~ _" [80] 80)
    1.17 +  znegative   :: int => bool
    1.18 +  zmagnitude  :: int => int
    1.19 +  zdiv,zmod   :: [int,int]=>int  (infixl 70)
    1.20 +  zpred,zsuc  :: int=>int
    1.21  
    1.22  defs
    1.23    zNat_def    "zNat == {x::nat. True}"