src/HOL/Real/Real.thy
author wenzelm
Mon, 07 Jan 2002 18:58:35 +0100
changeset 12655 b8c130dc46be
parent 9431 f921cca1067d
child 12734 c5f6d8259ecd
permissions -rw-r--r--
tuned;


Real = RComplete + RealPow