equal
deleted
inserted
replaced
50 done |
50 done |
51 |
51 |
52 |
52 |
53 subsection {* The set of rational numbers *} |
53 subsection {* The set of rational numbers *} |
54 |
54 |
55 constdefs |
55 definition |
56 rationals :: "real set" ("\<rat>") |
56 rationals :: "real set" ("\<rat>") |
57 "\<rat> \<equiv> {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 |
62 text {* |
62 text {* |