src/HOL/Real.thy
author nipkow
Thu Dec 11 08:56:02 2008 +0100 (2008-12-11)
changeset 29108 12ca66b887a0
parent 29026 5fbaa05f637f
child 29197 6d4cb27ed19c
permissions -rw-r--r--
codegen
     1 theory Real
     2 imports RComplete "~~/src/HOL/Real/RealVector"
     3 begin
     4 
     5 end