src/HOL/IntDef.thy
changeset 23477 f4b83f03cac9
parent 23438 dd824e86fa8a
child 23705 315c638d5856
     1.1 --- a/src/HOL/IntDef.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -137,13 +137,13 @@
     1.4    show "i - j = i + - j"
     1.5      by (simp add: diff_int_def)
     1.6    show "(i * j) * k = i * (j * k)"
     1.7 -    by (cases i, cases j, cases k) (simp add: mult ring_eq_simps)
     1.8 +    by (cases i, cases j, cases k) (simp add: mult ring_simps)
     1.9    show "i * j = j * i"
    1.10 -    by (cases i, cases j) (simp add: mult ring_eq_simps)
    1.11 +    by (cases i, cases j) (simp add: mult ring_simps)
    1.12    show "1 * i = i"
    1.13      by (cases i) (simp add: One_int_def mult)
    1.14    show "(i + j) * k = i * k + j * k"
    1.15 -    by (cases i, cases j, cases k) (simp add: add mult ring_eq_simps)
    1.16 +    by (cases i, cases j, cases k) (simp add: add mult ring_simps)
    1.17    show "0 \<noteq> (1::int)"
    1.18      by (simp add: Zero_int_def One_int_def)
    1.19  qed
    1.20 @@ -358,7 +358,7 @@
    1.21    also have "\<dots> = (\<exists>n. z - w = int n)"
    1.22      by (auto elim: zero_le_imp_eq_int)
    1.23    also have "\<dots> = (\<exists>n. z = w + int n)"
    1.24 -    by (simp only: group_eq_simps)
    1.25 +    by (simp only: group_simps)
    1.26    finally show ?thesis .
    1.27  qed
    1.28