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;
```