src/HOL/Real.thy
author blanchet
Thu, 18 Feb 2010 18:48:07 +0100
changeset 35220 2bcdae5f4fdb
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

theory Real
imports RComplete RealVector
begin

end