src/HOL/Real.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 26 Apr 2010 15:14:14 +0200
changeset 36352 f71978e47cd5
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
add bounded_lattice_bot and bounded_lattice_top type classes

theory Real
imports RComplete RealVector
begin

end