# HG changeset patch
# User chaieb
# Date 1179301522 -7200
# Node ID bff3fcdeecd38c3ffd0351239d94eb39902a2474
# Parent  cf071f3fc4aea0f3a565c5839cb2055763b2a829
dropped |R

diff -r cf071f3fc4ae -r bff3fcdeecd3 src/HOL/Library/Executable_Real.thy
--- 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