src/HOL/Hyperreal/Integration.thy

 lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)"
 by (simp add: partition)
 
 lemma lemma_partition_lt_gen [rule_format]:
  "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
-apply (induct_tac "d", auto simp add: partition)
+apply (induct "d", auto simp add: partition)
 apply (blast dest: Suc_le_lessD  intro: less_le_trans order_less_trans)
 done
 
 lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d"
 by (auto simp add: less_iff_Suc_add)

 apply auto
 done
 
 lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
 apply (frule partition [THEN iffD1], safe)
-apply (induct_tac "r")
-apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
- apply (blast intro: order_trans partition_le)
-apply (drule_tac x = n in spec)
-apply (best intro: order_less_trans order_trans order_less_imp_le)
+apply (induct "r")
+apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear)
+apply (auto intro: partition_le)
+apply (drule_tac x = r in spec)
+apply arith; 
 done
 
 lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
 apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)

 apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def)
 done
 
 lemma sumr_partition_eq_diff_bounds [simp]:
      "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
-by (induct_tac "m", auto)
+by (induct "m", auto)
 
 lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
 apply (auto simp add: order_le_less rsum_def Integral_def)
 apply (rule_tac x = "%x. b - a" in exI)
 apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)