src/HOL/Real/Real.thy
author obua
Tue, 23 Nov 2004 15:50:27 +0100
changeset 15314 55eec5c6d401
parent 14374 61de62096768
child 15536 3ce1cb7a24f0
permissions -rw-r--r--
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring


Real = RComplete + RealPow