dropped |R

--- a/src/HOL/Library/Executable_Real.thy	Tue May 15 18:28:02 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy	Wed May 16 09:45:22 2007 +0200
@@ -131,7 +131,7 @@
   "Nle \<equiv> \<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b)"
 
 
-subsection {* Interpretation of the normalized rats in \<real> *}
+subsection {* Interpretation of the normalized rats in reals *}
 
 definition
   INum:: "Num \<Rightarrow> real"
@@ -480,5 +480,4 @@
 *}
 
 consts_code INum ("")
-
 end
\ No newline at end of file