src/HOL/Nat.thy
 changeset 15251 bb6f072c8d10 parent 15140 322485b816ac child 15281 bd4611956c7b
```     1.1 --- a/src/HOL/Nat.thy	Mon Oct 18 13:40:45 2004 +0200
1.2 +++ b/src/HOL/Nat.thy	Tue Oct 19 18:18:45 2004 +0200
1.3 @@ -149,7 +149,7 @@
1.4  theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
1.5      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
1.6    apply (rule_tac x = m in spec)
1.7 -  apply (induct_tac n)
1.8 +  apply (induct n)
1.9    prefer 2
1.10    apply (rule allI)
1.11    apply (induct_tac x, rules+)
1.12 @@ -261,8 +261,8 @@
1.13
1.14  text {* "Less than" is a linear ordering *}
1.15  lemma less_linear: "m < n | m = n | n < (m::nat)"
1.16 -  apply (induct_tac m)
1.17 -  apply (induct_tac n)
1.18 +  apply (induct m)
1.19 +  apply (induct n)
1.20    apply (rule refl [THEN disjI1, THEN disjI2])
1.21    apply (rule zero_less_Suc [THEN disjI1])
1.22    apply (blast intro: Suc_mono less_SucI elim: lessE)
1.23 @@ -614,10 +614,10 @@
1.24  text {* Difference *}
1.25
1.26  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
1.27 -  by (induct_tac n) simp_all
1.28 +  by (induct n) simp_all
1.29
1.30  lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
1.31 -  by (induct_tac n) simp_all
1.32 +  by (induct n) simp_all
1.33
1.34
1.35  text {*
1.36 @@ -730,7 +730,7 @@
1.37  qed
1.38
1.39  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
1.40 -  apply (induct_tac m)
1.41 +  apply (induct m)
1.42    apply (induct_tac [2] n, simp_all)
1.43    done
1.44
1.45 @@ -743,7 +743,7 @@
1.46  text {* strict, in both arguments *}
1.47  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
1.48    apply (rule add_less_mono1 [THEN less_trans], assumption+)
1.49 -  apply (induct_tac j, simp_all)
1.50 +  apply (induct j, simp_all)
1.51    done
1.52
1.53  text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
1.54 @@ -999,8 +999,8 @@
1.55    done
1.56
1.57  lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
1.58 -  apply (induct_tac m, simp)
1.59 -  apply (induct_tac n, simp, fastsimp)
1.60 +  apply (induct m, simp)
1.61 +  apply (induct n, simp, fastsimp)
1.62    done
1.63
1.64  lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
```