| changeset 21404 | eb85850d3eb7 |
| parent 19736 | d8d0f8f51d69 |
| child 27651 | 16a26996c30e |
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy Fri Nov 17 02:20:03 2006 +0100 @@ -53,7 +53,7 @@ subsection {* The set of rational numbers *} definition - rationals :: "real set" ("\<rat>") + rationals :: "real set" ("\<rat>") where "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"