src/ZF/ex/Integ.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/ex/Integ.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/ex/Integ.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,17 +8,17 @@
     1.4  
     1.5  Integ = EquivClass + Arith +
     1.6  consts
     1.7 -    intrel,integ::      "i"
     1.8 -    znat	::	"i=>i"		("$# _" [80] 80)
     1.9 -    zminus	::	"i=>i"		("$~ _" [80] 80)
    1.10 -    znegative	::	"i=>o"
    1.11 -    zmagnitude	::	"i=>i"
    1.12 -    "$*"        ::      "[i,i]=>i"      (infixl 70)
    1.13 -    "$'/"       ::      "[i,i]=>i"      (infixl 70) 
    1.14 -    "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
    1.15 -    "$+"	::      "[i,i]=>i"      (infixl 65)
    1.16 -    "$-"        ::      "[i,i]=>i"      (infixl 65)
    1.17 -    "$<"	:: 	"[i,i]=>o"  	(infixl 50)
    1.18 +    intrel,integ::      i
    1.19 +    znat	::	i=>i		("$# _" [80] 80)
    1.20 +    zminus	::	i=>i		("$~ _" [80] 80)
    1.21 +    znegative	::	i=>o
    1.22 +    zmagnitude	::	i=>i
    1.23 +    "$*"        ::      [i,i]=>i      (infixl 70)
    1.24 +    "$'/"       ::      [i,i]=>i      (infixl 70) 
    1.25 +    "$'/'/"     ::      [i,i]=>i      (infixl 70)
    1.26 +    "$+"	::      [i,i]=>i      (infixl 65)
    1.27 +    "$-"        ::      [i,i]=>i      (infixl 65)
    1.28 +    "$<"	:: 	[i,i]=>o  	(infixl 50)
    1.29  
    1.30  defs
    1.31