# HG changeset patch
# User ballarin
# Date 1190717964 -7200
# Node ID 8e77a023d0809a1eb703bc91a0e60f147b5e1b84
# Parent  9a95634ab13544cff1069d0ab7c4b1b6f9b35570
Simplified proof due to improved integration of order_tac and simp.

diff -r 9a95634ab135 -r 8e77a023d080 src/HOL/List.thy
--- 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