equal
deleted
inserted
replaced
143 (* A positive fraction not in a positive real is an upper bound *) |
143 (* A positive fraction not in a positive real is an upper bound *) |
144 (* Gleason p. 122 - Remark (1) *) |
144 (* Gleason p. 122 - Remark (1) *) |
145 |
145 |
146 Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x"; |
146 Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x"; |
147 by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1); |
147 by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1); |
148 by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset())); |
148 by (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1); |
149 qed "not_in_preal_ub"; |
149 qed "not_in_preal_ub"; |
150 |
150 |
151 (* preal_less is a strong order i.e nonreflexive and transitive *) |
151 (* preal_less is a strong order i.e nonreflexive and transitive *) |
152 |
152 |
153 Goalw [preal_less_def] "~ (x::preal) < x"; |
153 Goalw [preal_less_def] "~ (x::preal) < x"; |