src/HOL/Real.thy
author wenzelm
Mon, 15 Feb 2010 23:58:24 +0100
changeset 35138 ad213c602ec1
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
refined and exported record_info;

theory Real
imports RComplete RealVector
begin

end