summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | bulwahn |

Fri, 21 Oct 2011 14:25:38 +0200 | |

changeset 45236 | ac4a2a66707d |

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 | file | annotate | diff | comparison | revisions | |

src/HOL/Library/List_Prefix.thy | file | annotate | diff | comparison | revisions |

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