src/HOL/Real/Real.thy
author oheimb
Fri, 11 Jul 2003 13:54:32 +0200
changeset 14097 f4d2ff3cad09
parent 12734 c5f6d8259ecd
child 14374 61de62096768
permissions -rw-r--r--
re-introduced sort constraints on LHS


Real = RComplete + Complex_Numbers