changeset 6993 | efb605156ca3 |
parent 6917 | eba301caceea |
child 7706 | da41066983e5 |
--- 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