src/HOL/Nat.ML

         rtac (lessI RS less_trans) 1,
         rtac (lessI RS Suc_mono) 1]);
 
 Goal "min 0 n = 0";
 by (rtac min_leastL 1);
-by (trans_tac 1);
+by (Simp_tac 1);
 qed "min_0L";
 
 Goal "min n 0 = 0";
 by (rtac min_leastR 1);
-by (trans_tac 1);
+by (Simp_tac 1);
 qed "min_0R";
 
 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
 by (Simp_tac 1);
 qed "min_Suc_Suc";