src/HOL/Real/Real.thy
author huffman
Tue Sep 12 07:49:07 2006 +0200 (2006-09-12)
changeset 20505 1e223f64bd59
parent 19640 40ec89317425
child 23454 c54975167be9
permissions -rw-r--r--
import RealVector
wenzelm@19640
     1
wenzelm@19640
     2
(* $Id$ *)
wenzelm@19640
     3
nipkow@15536
     4
theory Real
huffman@20505
     5
imports ContNotDenum Ferrante_Rackoff RealVector
nipkow@15536
     6
begin
wenzelm@19640
     7
end