src/HOL/Real.thy
changeset 29026 5fbaa05f637f
parent 28952 15a4b2cf8c34
child 29108 12ca66b887a0
     1.1 --- a/src/HOL/Real.thy	Thu Dec 04 14:17:36 2008 +0100
     1.2 +++ b/src/HOL/Real.thy	Wed Dec 10 10:23:47 2008 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Real
     1.5 -imports ContNotDenum "~~/src/HOL/Real/RealVector"
     1.6 +imports "~~/src/HOL/Real/RealVector"
     1.7  begin
     1.8  
     1.9  end