src/HOL/IntDef.thy
changeset 23282 dfc459989d24
parent 23276 a70934b63910
child 23299 292b1cbd05dc
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 06 19:12:59 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 06 20:49:04 2007 +0200
     1.3 @@ -669,16 +669,17 @@
     1.4  
     1.5  text{*Class for unital rings with characteristic zero.
     1.6   Includes non-ordered rings like the complex numbers.*}
     1.7 -axclass ring_char_0 < ring_1
     1.8 -  of_int_inject: "of_int w = of_int z ==> w = z"
     1.9 +axclass ring_char_0 < ring_1, semiring_char_0
    1.10  
    1.11  lemma of_int_eq_iff [simp]:
    1.12       "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
    1.13 -by (safe elim!: of_int_inject)
    1.14 +apply (cases w, cases z, simp add: of_int)
    1.15 +apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
    1.16 +apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
    1.17 +done
    1.18  
    1.19  text{*Every @{text ordered_idom} has characteristic zero.*}
    1.20 -instance ordered_idom < ring_char_0
    1.21 -by intro_classes (simp add: order_eq_iff)
    1.22 +instance ordered_idom < ring_char_0 ..
    1.23  
    1.24  text{*Special cases where either operand is zero*}
    1.25  lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]