src/HOL/Real/Real.thy
author nipkow
Tue Oct 23 23:27:23 2007 +0200 (2007-10-23)
changeset 25162 ad4d5365d9d8
parent 23454 c54975167be9
child 27964 1e0303048c0b
permissions -rw-r--r--
went back to >0
     1 
     2 (* $Id$ *)
     3 
     4 theory Real
     5 imports ContNotDenum RealVector
     6 begin
     7 end