Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/int_arith1.ML
changeset 14738 83f1a514dcb4
parent 14474 00292f6f8d13
child 15013 34264f5e4691 
--- a/src/HOL/Integ/int_arith1.ML	Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Tue May 11 20:11:08 2004 +0200
@@ -383,20 +383,20 @@
       "(l::'a::number_ring) = m * n"],
      EqCancelNumerals.proc),
     ("intless_cancel_numerals",
-     ["(l::'a::{ordered_ring,number_ring}) + m < n",
-      "(l::'a::{ordered_ring,number_ring}) < m + n",
-      "(l::'a::{ordered_ring,number_ring}) - m < n",
-      "(l::'a::{ordered_ring,number_ring}) < m - n",
-      "(l::'a::{ordered_ring,number_ring}) * m < n",
-      "(l::'a::{ordered_ring,number_ring}) < m * n"],
+     ["(l::'a::{ordered_idom,number_ring}) + m < n",
+      "(l::'a::{ordered_idom,number_ring}) < m + n",
+      "(l::'a::{ordered_idom,number_ring}) - m < n",
+      "(l::'a::{ordered_idom,number_ring}) < m - n",
+      "(l::'a::{ordered_idom,number_ring}) * m < n",
+      "(l::'a::{ordered_idom,number_ring}) < m * n"],
      LessCancelNumerals.proc),
     ("intle_cancel_numerals",
-     ["(l::'a::{ordered_ring,number_ring}) + m <= n",
-      "(l::'a::{ordered_ring,number_ring}) <= m + n",
-      "(l::'a::{ordered_ring,number_ring}) - m <= n",
-      "(l::'a::{ordered_ring,number_ring}) <= m - n",
-      "(l::'a::{ordered_ring,number_ring}) * m <= n",
-      "(l::'a::{ordered_ring,number_ring}) <= m * n"],
+     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
+      "(l::'a::{ordered_idom,number_ring}) <= m + n",
+      "(l::'a::{ordered_idom,number_ring}) - m <= n",
+      "(l::'a::{ordered_idom,number_ring}) <= m - n",
+      "(l::'a::{ordered_idom,number_ring}) * m <= n",
+      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
      LeCancelNumerals.proc)];
 
 
@@ -488,7 +488,7 @@
 
 val assoc_fold_simproc =
   Bin_Simprocs.prep_simproc
-   ("semiring_assoc_fold", ["(a::'a::semiring) * b"],
+   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
     Semiring_Times_Assoc.proc);
 
 Addsimprocs [assoc_fold_simproc];
@@ -545,9 +545,9 @@
 val fast_int_arith_simproc =
   Simplifier.simproc (Theory.sign_of (the_context()))
   "fast_int_arith" 
-     ["(m::'a::{ordered_ring,number_ring}) < n",
-      "(m::'a::{ordered_ring,number_ring}) <= n",
-      "(m::'a::{ordered_ring,number_ring}) = n"] Fast_Arith.lin_arith_prover;
+     ["(m::'a::{ordered_idom,number_ring}) < n",
+      "(m::'a::{ordered_idom,number_ring}) <= n",
+      "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
 
 Addsimprocs [fast_int_arith_simproc]
isabelle