src/HOL/IntDiv.thy
changeset 25571 c9e39eafc7a0
parent 25134 3d4953e88449
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/IntDiv.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -62,9 +62,18 @@
     1.4                    if 0<b then negDivAlg a b
     1.5                    else negateSnd (posDivAlg (-a) (-b))))"
     1.6  
     1.7 -instance int :: Divides.div
     1.8 -  div_def: "a div b == fst (divAlg (a, b))"
     1.9 -  mod_def: "a mod b == snd (divAlg (a, b))" ..
    1.10 +instantiation int :: Divides.div
    1.11 +begin
    1.12 +
    1.13 +definition
    1.14 +  div_def: "a div b = fst (divAlg (a, b))"
    1.15 +
    1.16 +definition
    1.17 +  mod_def: "a mod b = snd (divAlg (a, b))"
    1.18 +
    1.19 +instance ..
    1.20 +
    1.21 +end
    1.22  
    1.23  lemma divAlg_mod_div:
    1.24    "divAlg (p, q) = (p div q, p mod q)"