equal
deleted
inserted
replaced
51 |
51 |
52 |
52 |
53 subsection {* The set of rational numbers *} |
53 subsection {* The set of rational numbers *} |
54 |
54 |
55 definition |
55 definition |
56 rationals :: "real set" ("\<rat>") |
56 rationals :: "real set" ("\<rat>") where |
57 "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
57 "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
58 |
58 |
59 |
59 |
60 subsection {* Main theorem *} |
60 subsection {* Main theorem *} |
61 |
61 |