src/HOL/Real.thy
author nipkow
Wed Dec 10 10:23:47 2008 +0100 (2008-12-10)
changeset 29026 5fbaa05f637f
parent 28952 15a4b2cf8c34
child 29108 12ca66b887a0
permissions -rw-r--r--
moved ContNotDenum into Library
     1 theory Real
     2 imports "~~/src/HOL/Real/RealVector"
     3 begin
     4 
     5 end