src/HOL/Real/ex/BinEx.ML
Thu, 23 Sep 1999 18:39:05 +0200 paulson Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
Wed, 22 Sep 1999 21:04:34 +0200 wenzelm proper theory setup for Real/ex/BinEx;
Mon, 30 Aug 1999 15:25:16 +0200 paulson new directory HOL/Real/ex of real examples
less more (0) tip