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

author | kleing |

Tue, 13 Apr 2004 07:48:32 +0200 | |

changeset 14550 | b13da5649bf9 |

parent 14549 | ea6e18e5c7a9 |

child 14551 | 2cb6ff394bfb |

hence -> from calculation have

--- a/src/HOL/Real/PReal.thy Tue Apr 13 07:47:31 2004 +0200 +++ b/src/HOL/Real/PReal.thy Tue Apr 13 07:48:32 2004 +0200 @@ -388,15 +388,16 @@ show "x * y \<notin> mult_set A B" proof - { fix u::rat and v::rat - assume "u \<in> A" and "v \<in> B" and "x*y = u*v" - moreover - with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+ - moreover - with prems have "0\<le>v" - by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems) - moreover - hence "u*v < x*y" by (blast intro: mult_strict_mono prems) - ultimately have False by force} + assume "u \<in> A" and "v \<in> B" and "x*y = u*v" + moreover + with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+ + moreover + with prems have "0\<le>v" + by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems) + moreover + from calculation + have "u*v < x*y" by (blast intro: mult_strict_mono prems) + ultimately have False by force } thus ?thesis by (auto simp add: mult_set_def) qed qed