src/HOL/Real.thy
author nipkow
Wed, 10 Dec 2008 10:23:47 +0100
changeset 29026 5fbaa05f637f
parent 28952 15a4b2cf8c34
child 29108 12ca66b887a0
permissions -rw-r--r--
moved ContNotDenum into Library

theory Real
imports "~~/src/HOL/Real/RealVector"
begin

end