src/HOL/Numeral_Simprocs.thy
changeset 45296 7a97b2bda137
parent 45284 ae78a4ffa81d
child 45308 2e84e5f0463b
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sat Oct 29 00:23:58 2011 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Oct 28 16:49:15 2011 +0200
     1.3 @@ -165,13 +165,13 @@
     1.4    {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
     1.5  
     1.6  simproc_setup linordered_ring_le_cancel_factor
     1.7 -  ("(l::'a::linordered_ring) * m <= n"
     1.8 -  |"(l::'a::linordered_ring) <= m * n") =
     1.9 +  ("(l::'a::linordered_idom) * m <= n"
    1.10 +  |"(l::'a::linordered_idom) <= m * n") =
    1.11    {* fn phi => Numeral_Simprocs.le_cancel_factor *}
    1.12  
    1.13  simproc_setup linordered_ring_less_cancel_factor
    1.14 -  ("(l::'a::linordered_ring) * m < n"
    1.15 -  |"(l::'a::linordered_ring) < m * n") =
    1.16 +  ("(l::'a::linordered_idom) * m < n"
    1.17 +  |"(l::'a::linordered_idom) < m * n") =
    1.18    {* fn phi => Numeral_Simprocs.less_cancel_factor *}
    1.19  
    1.20  simproc_setup int_div_cancel_factor