# HG changeset patch
# User paulson
# Date 971087052 -7200
# Node ID 1d097572d23bccae43e865641e9a27fde707f33f
# Parent  3daeda3d3cd030ec6593043ce8bff998728c8bad
got rid of a swap

diff -r 3daeda3d3cd0 -r 1d097572d23b src/HOL/Nat.ML
--- 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];