src/HOL/Hyperreal/StarClasses.thy

 apply (transfer, erule (1) mult_strict_left_mono)
 apply (transfer, erule (1) mult_strict_right_mono)
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono1)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
 
 instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
 by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)

 qed
 
 subsection {* Number classes *}
 
 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
-by (induct_tac n, simp_all)
+by (induct n, simp_all)
 
 lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
 by (simp add: star_of_nat_def)
 
 lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"