src/HOL/IOA/IOA.thy

--- a/src/HOL/IOA/IOA.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/IOA/IOA.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -251,9 +251,7 @@
    apply (rule_tac x = "Suc n" in exI)
    apply (simp (no_asm))
   apply simp
-  apply (rule allI)
-  apply (cut_tac m = "na" and n = "n" in less_linear)
-  apply auto
+  apply (metis ioa_triple_proj less_antisym)
   done