--- 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
--- 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)"