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);
```