| changeset 35028 | 108662d50512 |
| parent 34944 | 970e1466028d |
| child 35687 | 564a49e8be44 |
--- a/src/HOL/Code_Numeral.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Feb 05 14:33:50 2010 +0100 @@ -144,7 +144,7 @@ subsection {* Basic arithmetic *} -instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" +instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}" begin definition [simp, code del]: