src/HOL/Nat.ML
changeset 6301 08245f5a436d
parent 6115 c70bce7deb0f
child 6433 228237ec56e5
     1.1 --- a/src/HOL/Nat.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4  AddIffs [neq0_conv];
     1.5  
     1.6  Goal "(0 ~= n) = (0 < n)";
     1.7 -by(exhaust_tac "n" 1);
     1.8 -by(Auto_tac);
     1.9 +by (exhaust_tac "n" 1);
    1.10 +by (Auto_tac);
    1.11  qed "zero_neq_conv";
    1.12  AddIffs [zero_neq_conv];
    1.13