replacing metis proofs with facts xt1 by new proof with more readable names
authorbulwahn
Fri Oct 21 14:25:38 2011 +0200 (2011-10-21)
changeset 45236ac4a2a66707d
parent 45235 7187bce94e88
child 45237 769c4cbcd319
replacing metis proofs with facts xt1 by new proof with more readable names
src/HOL/Library/Extended_Real.thy
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Oct 21 14:06:15 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Oct 21 14:25:38 2011 +0200
     1.3 @@ -1362,8 +1362,7 @@
     1.4  }
     1.5  moreover
     1.6  { assume "?lhs" hence "?rhs"
     1.7 -  by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
     1.8 -      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
     1.9 +  by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
    1.10  } ultimately show ?thesis by auto
    1.11  qed
    1.12  
    1.13 @@ -1382,8 +1381,7 @@
    1.14  }
    1.15  moreover
    1.16  { assume "?lhs" hence "?rhs"
    1.17 -  by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
    1.18 -      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
    1.19 +  by (metis INF_less_iff order_le_less order_less_le_trans)
    1.20  } ultimately show ?thesis by auto
    1.21  qed
    1.22  
     2.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:06:15 2011 +0200
     2.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:25:38 2011 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4  next
     2.5    assume "xs = ys @ [y] \<or> xs \<le> ys"
     2.6    then show "xs \<le> ys @ [y]"
     2.7 -    by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
     2.8 +    by (metis order_eq_iff order_trans prefixI)
     2.9  qed
    2.10  
    2.11  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"