src/HOL/IntDiv.thy
changeset 28562 4e74209f113e
parent 28262 aa7ca36d67fd
child 29045 3c8f48333731
     1.1 --- a/src/HOL/IntDiv.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -14,13 +14,13 @@
     1.4  constdefs
     1.5    quorem :: "(int*int) * (int*int) => bool"
     1.6      --{*definition of quotient and remainder*}
     1.7 -    [code func]: "quorem == %((a,b), (q,r)).
     1.8 +    [code]: "quorem == %((a,b), (q,r)).
     1.9                        a = b*q + r &
    1.10                        (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
    1.11  
    1.12    adjust :: "[int, int*int] => int*int"
    1.13      --{*for the division algorithm*}
    1.14 -    [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    1.15 +    [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    1.16                           else (2*q, r)"
    1.17  
    1.18  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
    1.19 @@ -46,7 +46,7 @@
    1.20  text{*algorithm for the general case @{term "b\<noteq>0"}*}
    1.21  constdefs
    1.22    negateSnd :: "int*int => int*int"
    1.23 -    [code func]: "negateSnd == %(q,r). (q,-r)"
    1.24 +    [code]: "negateSnd == %(q,r). (q,-r)"
    1.25  
    1.26  definition
    1.27    divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
    1.28 @@ -1477,7 +1477,7 @@
    1.29  context ring_1
    1.30  begin
    1.31  
    1.32 -lemma of_int_num [code func]:
    1.33 +lemma of_int_num [code]:
    1.34    "of_int k = (if k = 0 then 0 else if k < 0 then
    1.35       - of_int (- k) else let
    1.36         (l, m) = divAlg (k, 2);