Up to index of Isabelle/HOL/HOL-Algebra/example_Bicomplex
(* $Id: Real.thy,v 1.15 2007/06/21 13:42:07 wenzelm Exp $ *) theory Real imports ContNotDenum RealVector begin end