src/HOL/arith_data.ML
changeset 4309 c98f44948d86
parent 4295 81132a38996a
child 4310 cad4f24be60b
     1.1 --- a/src/HOL/arith_data.ML	Wed Nov 26 17:35:46 1997 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Wed Nov 26 17:52:53 1997 +0100
     1.3 @@ -7,10 +7,12 @@
     1.4  
     1.5  signature ARITH_DATA =
     1.6  sig
     1.7 +  val nat_cancel_sums: simproc list
     1.8 +  val nat_cancel_factor: simproc list
     1.9    val nat_cancel: simproc list
    1.10  end;
    1.11  
    1.12 -structure ArithData (* FIXME :ARITH_DATA *) =
    1.13 +structure ArithData: ARITH_DATA =
    1.14  struct
    1.15  
    1.16  
    1.17 @@ -182,13 +184,17 @@
    1.18  val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
    1.19  val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
    1.20  
    1.21 -val nat_cancel = map prep_simproc
    1.22 -  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
    1.23 -   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
    1.24 -   ("natle_cancel_factor", le_pats, LeCancelFactor.proc),
    1.25 -   ("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    1.26 +val nat_cancel_sums = map prep_simproc
    1.27 +  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
    1.28     ("natless_cancel_sums", less_pats, LessCancelSums.proc),
    1.29     ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
    1.30  
    1.31 +val nat_cancel_factor = map prep_simproc
    1.32 +  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
    1.33 +   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
    1.34 +   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
    1.35 +
    1.36 +val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
    1.37 +
    1.38  
    1.39  end;