more accurate class constraints on cancellation simproc patterns
authorhuffman
Fri, 28 Oct 2011 16:49:15 +0200
changeset 45296 7a97b2bda137
parent 45295 255200892a42
child 45297 3c9f17d017bf
child 45306 1e380c50a183
more accurate class constraints on cancellation simproc patterns
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