src/HOL/Real.thy
author haftmann
Mon, 26 Apr 2010 11:34:15 +0200
changeset 36348 89c54f51f55a
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero

theory Real
imports RComplete RealVector
begin

end