Integrated Executable_Rat and Executable_Real theories into
Rational and RealDef theories.

--- a/src/HOL/Library/Library.thy	Wed Sep 05 21:09:11 2007 +0200
+++ b/src/HOL/Library/Library.thy	Thu Sep 06 11:32:28 2007 +0200
@@ -14,8 +14,6 @@
   Efficient_Nat
   Eval
   Eval_Witness
-  Executable_Rat
-  Executable_Real
   Executable_Set
   FuncSet
   GCD

--- a/src/HOL/ex/Codegenerator_Pretty.thy	Wed Sep 05 21:09:11 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Thu Sep 06 11:32:28 2007 +0200
@@ -6,7 +6,7 @@
 header {* Simple examples for pretty numerals and such *}
 
 theory Codegenerator_Pretty
-imports Executable_Rat Executable_Real Efficient_Nat
+imports "~~/src/HOL/Real/RealDef" Efficient_Nat
 begin
 
 definition

--- a/src/HOL/ex/ExecutableContent.thy	Wed Sep 05 21:09:11 2007 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Thu Sep 06 11:32:28 2007 +0200
@@ -13,8 +13,7 @@
   Binomial
   Commutative_Ring
   "~~/src/HOL/ex/Commutative_Ring_Complete"
-  Executable_Rat
-  Executable_Real
+  "~~/src/HOL/Real/RealDef"
   GCD
   List_Prefix
   Nat_Infinity

--- a/src/HOL/ex/ROOT.ML	Wed Sep 05 21:09:11 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Sep 06 11:32:28 2007 +0200
@@ -53,7 +53,6 @@
 no_document time_use_thy "Pretty_Int";
 time_use_thy "Random";
 
-no_document time_use_thy "Executable_Rat";
 no_document time_use_thy "Efficient_Nat";
 no_document time_use_thy "Codegenerator";
 no_document time_use_thy "Codegenerator_Pretty";