src/ZF/Integ/Int.thy
changeset 9578 ab26d6c8ebfe
parent 9570 e16e168984e1
child 9654 9754ba005b64
     1.1 --- a/src/ZF/Integ/Int.thy	Fri Aug 11 13:26:40 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.thy	Fri Aug 11 13:27:17 2000 +0200
     1.3 @@ -67,10 +67,4 @@
     1.4    zle          ::      [i,i]=>o      (infixl "$<=" 50)
     1.5       "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
     1.6    
     1.7 -(*div and mod await definitions!*)
     1.8 -consts
     1.9 -  "$'/"       ::      [i,i]=>i      (infixl 70) 
    1.10 -
    1.11 -  "$'/'/"     ::      [i,i]=>i      (infixl 70)
    1.12 -    
    1.13  end