--- a/src/HOL/Nat.ML Mon Oct 09 12:23:45 2000 +0200 +++ b/src/HOL/Nat.ML Mon Oct 09 12:24:12 2000 +0200 @@ -58,7 +58,7 @@ Goal "!!n::nat. (~(0 < n)) = (n=0)"; by (rtac iffI 1); - by (etac swap 1); + by (rtac ccontr 1); by (ALLGOALS Asm_full_simp_tac); qed "not_gr0"; AddIffs [not_gr0];