src/HOL/Tools/numeral_simprocs.ML
changeset 36349 39be26d1bc28
parent 35983 27e2fa7d4ce7
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -332,8 +332,8 @@
     1.4  val field_combine_numerals =
     1.5    Arith_Data.prep_simproc @{theory}
     1.6      ("field_combine_numerals", 
     1.7 -     ["(i::'a::{number_ring,field,division_by_zero}) + j",
     1.8 -      "(i::'a::{number_ring,field,division_by_zero}) - j"], 
     1.9 +     ["(i::'a::{number_ring,field,division_ring_inverse_zero}) + j",
    1.10 +      "(i::'a::{number_ring,field,division_ring_inverse_zero}) - j"], 
    1.11       K FieldCombineNumerals.proc);
    1.12  
    1.13  (** Constant folding for multiplication in semirings **)
    1.14 @@ -442,9 +442,9 @@
    1.15        "(l::'a::{semiring_div,number_ring}) div (m * n)"],
    1.16       K DivCancelNumeralFactor.proc),
    1.17      ("divide_cancel_numeral_factor",
    1.18 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
    1.19 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
    1.20 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
    1.21 +     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
    1.22 +      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
    1.23 +      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
    1.24       K DivideCancelNumeralFactor.proc)];
    1.25  
    1.26  val field_cancel_numeral_factors =
    1.27 @@ -454,9 +454,9 @@
    1.28        "(l::'a::{field,number_ring}) = m * n"],
    1.29       K EqCancelNumeralFactor.proc),
    1.30      ("field_cancel_numeral_factor",
    1.31 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
    1.32 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
    1.33 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
    1.34 +     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
    1.35 +      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
    1.36 +      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
    1.37       K DivideCancelNumeralFactor.proc)]
    1.38  
    1.39  
    1.40 @@ -598,8 +598,8 @@
    1.41       ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
    1.42       K DvdCancelFactor.proc),
    1.43      ("divide_cancel_factor",
    1.44 -     ["((l::'a::{division_by_zero,field}) * m) / n",
    1.45 -      "(l::'a::{division_by_zero,field}) / (m * n)"],
    1.46 +     ["((l::'a::{division_ring_inverse_zero,field}) * m) / n",
    1.47 +      "(l::'a::{division_ring_inverse_zero,field}) / (m * n)"],
    1.48       K DivideCancelFactor.proc)];
    1.49  
    1.50  end;