equal
deleted
inserted
replaced
1656 |
1656 |
1657 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" |
1657 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" |
1658 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) |
1658 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) |
1659 |
1659 |
1660 |
1660 |
1661 subsection{*Numerals and Arithmetic*} |
|
1662 |
|
1663 instantiation real :: number_ring |
|
1664 begin |
|
1665 |
|
1666 definition |
|
1667 real_number_of_def: "(number_of w :: real) = of_int w" |
|
1668 |
|
1669 instance |
|
1670 by intro_classes (simp add: real_number_of_def) |
|
1671 |
|
1672 end |
|
1673 |
|
1674 subsection {* Completeness of Positive Reals *} |
1661 subsection {* Completeness of Positive Reals *} |
1675 |
1662 |
1676 text {* |
1663 text {* |
1677 Supremum property for the set of positive reals |
1664 Supremum property for the set of positive reals |
1678 |
1665 |