src/HOL/Nat.ML
changeset 4686 74a12e86b20b
parent 3023 01364e2f30ad
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Nat.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/Nat.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -15,7 +15,6 @@
     1.4  qed "min_0R";
     1.5  
     1.6  goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
     1.7 -by (split_tac [expand_if] 1);
     1.8  by (Simp_tac 1);
     1.9  qed "min_Suc_Suc";
    1.10