author | paulson |
Tue, 13 Jul 1999 10:45:47 +0200 (1999-07-13) | |
changeset 6993 | efb605156ca3 |
parent 6992 | 8113992d3f45 |
child 6994 | f22a51ed9f11 |
--- a/src/HOL/Integ/IntDiv.thy Tue Jul 13 10:45:09 1999 +0200 +++ b/src/HOL/Integ/IntDiv.thy Tue Jul 13 10:45:47 1999 +0200 @@ -45,7 +45,7 @@ divAlg :: "int*int => int*int" "divAlg == %(a,b). if #0<=a then - if #0<b then posDivAlg (a,b) + if #0<=b then posDivAlg (a,b) else if a=#0 then (#0,#0) else negateSnd (negDivAlg (-a,-b)) else