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