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