src/HOL/Real.thy
author nipkow
Thu, 11 Dec 2008 08:56:02 +0100
changeset 29108 12ca66b887a0
parent 29026 5fbaa05f637f
child 29197 6d4cb27ed19c
permissions -rw-r--r--
codegen

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

end