# HG changeset patch
# User bulwahn
# Date 1319199938 -7200
# Node ID ac4a2a66707d74e76d9a33726d45e458a89d3e58
# Parent  7187bce94e889d900f59d5e0b5e7fa493dededae
replacing metis proofs with facts xt1 by new proof with more readable names

diff -r 7187bce94e88 -r ac4a2a66707d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Oct 21 14:06:15 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Oct 21 14:25:38 2011 +0200
@@ -1362,8 +1362,7 @@
 }
 moreover
 { assume "?lhs" hence "?rhs"
-  by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
-      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+  by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
 } ultimately show ?thesis by auto
 qed
 
@@ -1382,8 +1381,7 @@
 }
 moreover
 { assume "?lhs" hence "?rhs"
-  by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
-      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+  by (metis INF_less_iff order_le_less order_less_le_trans)
 } ultimately show ?thesis by auto
 qed
 
diff -r 7187bce94e88 -r ac4a2a66707d src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:06:15 2011 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:25:38 2011 +0200
@@ -74,7 +74,7 @@
 next
   assume "xs = ys @ [y] \<or> xs \<le> ys"
   then show "xs \<le> ys @ [y]"
-    by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
+    by (metis order_eq_iff order_trans prefixI)
 qed
 
 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"