src/HOL/Real.thy
author haftmann
Tue, 11 May 2010 18:46:03 +0200
changeset 36832 e6078ef937df
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
tuned reification functions

theory Real
imports RComplete RealVector
begin

end