Simplified proof due to improved integration of order_tac and simp.

--- a/src/HOL/List.thy	Tue Sep 25 12:56:27 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 25 12:59:24 2007 +0200
@@ -2578,10 +2578,7 @@
     done
 next
   assume "~ i \<sqsubseteq> j" thus ?thesis
-    apply(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
-    apply(subst atLeastAtMost_empty) apply simp
-    apply(simp cong:conj_cong)
-    done (* FIXME should reduce to the first simp alone *)
+    by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
 qed
 
 end