# HG changeset patch
# User wenzelm
# Date 880563173 -3600
# Node ID c98f44948d8695d0251a27b77d0b86926ff8ee72
# Parent  9abce31cc7646422190dac85922462fa6cb757ae
separate lists of simprocs;

diff -r 9abce31cc764 -r c98f44948d86 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Nov 26 17:35:46 1997 +0100
+++ b/src/HOL/arith_data.ML	Wed Nov 26 17:52:53 1997 +0100
@@ -7,10 +7,12 @@
 
 signature ARITH_DATA =
 sig
+  val nat_cancel_sums: simproc list
+  val nat_cancel_factor: simproc list
   val nat_cancel: simproc list
 end;
 
-structure ArithData (* FIXME :ARITH_DATA *) =
+structure ArithData: ARITH_DATA =
 struct
 
 
@@ -182,13 +184,17 @@
 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
 
-val nat_cancel = map prep_simproc
-  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
-   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
-   ("natle_cancel_factor", le_pats, LeCancelFactor.proc),
-   ("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
+val nat_cancel_sums = map prep_simproc
+  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
    ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
 
+val nat_cancel_factor = map prep_simproc
+  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
+   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
+   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
+
+val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
+
 
 end;