| changeset 19736 | d8d0f8f51d69 |
| parent 16663 | 13e9c402308b |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:00 2006 +0200 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:02 2006 +0200 @@ -52,9 +52,9 @@ subsection {* The set of rational numbers *} -constdefs +definition rationals :: "real set" ("\<rat>") - "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" + "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" subsection {* Main theorem *}