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
wenzelm@19640
     1
wenzelm@19640
     2
(* $Id$ *)
wenzelm@19640
     3
nipkow@15536
     4
theory Real
wenzelm@23454
     5
imports ContNotDenum RealVector
nipkow@15536
     6
begin
wenzelm@19640
     7
end