src/ZF/Integ/Int.thy
changeset 9333 5cacc383157a
parent 5561 426c1e330903
child 9496 07e33cac5d9c
     1.1 --- a/src/ZF/Integ/Int.thy	Thu Jul 13 23:26:08 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.thy	Fri Jul 14 13:39:03 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4       "intrel == {p:(nat*nat)*(nat*nat).                 
     1.5          EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
     1.6  
     1.7 -    int_def   "int == (nat*nat)/intrel"
     1.8 +    int_def   "int == (nat*nat)//intrel"
     1.9      
    1.10      int_of_def  "$# m == intrel `` {<m,0>}"
    1.11