# 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