equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 header {* Positive real numbers *} |
9 header {* Positive real numbers *} |
10 |
10 |
11 theory PReal |
11 theory PReal |
12 imports Rational "~~/src/HOL/Library/Dense_Linear_Order" |
12 imports Rational Dense_Linear_Order |
13 begin |
13 begin |
14 |
14 |
15 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
15 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
17 by (rule_tac x="b-a" in exI, simp) |
17 by (rule_tac x="b-a" in exI, simp) |