src/HOL/Real/Real.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 14374 61de62096768
child 15536 3ce1cb7a24f0
permissions -rw-r--r--
New theory header syntax.
     1 
     2 Real = RComplete + RealPow