remove Real.thy
authorhoelzl
Tue, 26 Mar 2013 12:20:56 +0100
changeset 51522 bd568f4bf446
parent 51521 36fa825e0ea7
child 51523 97b5e8a1291c
remove Real.thy
src/HOL/Complex_Main.thy
src/HOL/Real.thy
src/HOL/RealDef.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
--- 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
--- 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