src/HOL/Real/Real.thy
author paulson
Thu Sep 23 18:39:05 1999 +0200 (1999-09-23)
changeset 7588 26384af93359
parent 7562 8519d5019309
child 9431 f921cca1067d
permissions -rw-r--r--
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
RealAbs. RealAbs proofs have been highly streamlined. A couple of RealPow
proofs use #1, #2, etc.
     1 
     2 Real = Main + RComplete + RealPow