# HG changeset patch
# User hoelzl
# Date 1364296856 -3600
# Node ID bd568f4bf446e7cb6b2f5b1c6ce8d27c1a62694f
# Parent  36fa825e0ea7999106841cdc899d14aa96019111
remove Real.thy

diff -r 36fa825e0ea7 -r bd568f4bf446 src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Tue Mar 26 12:20:55 2013 +0100
+++ b/src/HOL/Complex_Main.thy	Tue Mar 26 12:20:56 2013 +0100
@@ -3,7 +3,6 @@
 theory Complex_Main
 imports
   Main
-  Real
   Complex
   Log
   Ln
diff -r 36fa825e0ea7 -r bd568f4bf446 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Mar 26 12:20:55 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Real
-imports RealVector
-begin
-
-ML_file "Tools/SMT/smt_real.ML"
-setup SMT_Real.setup
-
-end
diff -r 36fa825e0ea7 -r bd568f4bf446 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Mar 26 12:20:55 2013 +0100
+++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:56 2013 +0100
@@ -2223,4 +2223,7 @@
     times_real_inst.times_real uminus_real_inst.uminus_real
     zero_real_inst.zero_real
 
+ML_file "Tools/SMT/smt_real.ML"
+setup SMT_Real.setup
+
 end