src/HOL/Divides.thy
changeset 10559 d3fd54fc659b
parent 10214 77349ed89f45
child 10789 260fa2c67e3e
     1.1 --- a/src/HOL/Divides.thy	Fri Dec 01 11:02:55 2000 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Dec 01 11:03:31 2000 +0100
     1.3 @@ -36,4 +36,12 @@
     1.4  (*The definition of dvd is polymorphic!*)
     1.5    dvd_def   "m dvd n == EX k. n = m*k"
     1.6  
     1.7 +(*This definition helps prove the harder properties of div and mod.
     1.8 +  It is copied from IntDiv.thy; should it be overloaded?*)
     1.9 +constdefs
    1.10 +  quorem :: "(nat*nat) * (nat*nat) => bool"
    1.11 +    "quorem == %((a,b), (q,r)).
    1.12 +                      a = b*q + r &
    1.13 +                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
    1.14 +
    1.15  end