changeset 10789 | 260fa2c67e3e |
parent 10559 | d3fd54fc659b |
child 12338 | de0f4a63baa5 |
--- a/src/HOL/Divides.thy Fri Jan 05 13:10:37 2001 +0100 +++ b/src/HOL/Divides.thy Fri Jan 05 14:28:10 2001 +0100 @@ -19,7 +19,7 @@ consts div :: ['a::div, 'a] => 'a (infixl 70) mod :: ['a::div, 'a] => 'a (infixl 70) - dvd :: ['a::times, 'a] => bool (infixl 70) + dvd :: ['a::times, 'a] => bool (infixl 50) (*Remainder and quotient are defined here by algorithms and later proved to