src/HOL/Nat.ML
changeset 10173 1d097572d23b
parent 9969 4753185f1dd2
child 10450 60ddd5fdf93b
     1.1 --- a/src/HOL/Nat.ML	Mon Oct 09 12:23:45 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Oct 09 12:24:12 2000 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  
     1.5  Goal "!!n::nat. (~(0 < n)) = (n=0)";
     1.6  by (rtac iffI 1);
     1.7 - by (etac swap 1);
     1.8 + by (rtac ccontr 1);
     1.9   by (ALLGOALS Asm_full_simp_tac);
    1.10  qed "not_gr0";
    1.11  AddIffs [not_gr0];