--- a/src/HOL/Nat.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Nat.ML Sat Mar 07 16:29:29 1998 +0100
@@ -15,7 +15,6 @@
qed "min_0R";
goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
-by (split_tac [expand_if] 1);
by (Simp_tac 1);
qed "min_Suc_Suc";