# HG changeset patch
# User berghofe
# Date 1189071148 -7200
# Node ID 1bac2587911799cfbb8808218a86131257550890
# Parent  afd2be8a9aba02c90bc27ab16d12a641f366ef43
Integrated Executable_Rat and Executable_Real theories into
Rational and RealDef theories.

diff -r afd2be8a9aba -r 1bac25879117 src/HOL/Library/Library.thy
--- 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
diff -r afd2be8a9aba -r 1bac25879117 src/HOL/ex/Codegenerator_Pretty.thy
--- 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
diff -r afd2be8a9aba -r 1bac25879117 src/HOL/ex/ExecutableContent.thy
--- 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
diff -r afd2be8a9aba -r 1bac25879117 src/HOL/ex/ROOT.ML
--- 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";