# HG changeset patch # User huffman # Date 1319813355 -7200 # Node ID 7a97b2bda137a8a0e6e78d73721a6682e41446d5 # Parent 255200892a421fe6817deca8ab40754d1b124b1a more accurate class constraints on cancellation simproc patterns diff -r 255200892a42 -r 7a97b2bda137 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Sat Oct 29 00:23:58 2011 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Fri Oct 28 16:49:15 2011 +0200 @@ -165,13 +165,13 @@ {* fn phi => Numeral_Simprocs.eq_cancel_factor *} simproc_setup linordered_ring_le_cancel_factor - ("(l::'a::linordered_ring) * m <= n" - |"(l::'a::linordered_ring) <= m * n") = + ("(l::'a::linordered_idom) * m <= n" + |"(l::'a::linordered_idom) <= m * n") = {* fn phi => Numeral_Simprocs.le_cancel_factor *} simproc_setup linordered_ring_less_cancel_factor - ("(l::'a::linordered_ring) * m < n" - |"(l::'a::linordered_ring) < m * n") = + ("(l::'a::linordered_idom) * m < n" + |"(l::'a::linordered_idom) < m * n") = {* fn phi => Numeral_Simprocs.less_cancel_factor *} simproc_setup int_div_cancel_factor