dropped |R
authorchaieb
Wed May 16 09:45:22 2007 +0200 (2007-05-16)
changeset 22982bff3fcdeecd3
parent 22981 cf071f3fc4ae
child 22983 3314057c3b57
dropped |R
src/HOL/Library/Executable_Real.thy
     1.1 --- a/src/HOL/Library/Executable_Real.thy	Tue May 15 18:28:02 2007 +0200
     1.2 +++ b/src/HOL/Library/Executable_Real.thy	Wed May 16 09:45:22 2007 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    "Nle \<equiv> \<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b)"
     1.5  
     1.6  
     1.7 -subsection {* Interpretation of the normalized rats in \<real> *}
     1.8 +subsection {* Interpretation of the normalized rats in reals *}
     1.9  
    1.10  definition
    1.11    INum:: "Num \<Rightarrow> real"
    1.12 @@ -480,5 +480,4 @@
    1.13  *}
    1.14  
    1.15  consts_code INum ("")
    1.16 -
    1.17  end
    1.18 \ No newline at end of file