src/HOL/Real/RealArith.ML
Thu, 14 Dec 2000 10:30:11 +0100 paulson new theorem real_lbound_gt_zero
Wed, 13 Dec 2000 10:34:45 +0100 paulson another round of tidying-up
Tue, 12 Dec 2000 12:01:19 +0100 paulson first stage in tidying up Real and Hyperreal.
Fri, 01 Dec 2000 19:53:29 +0100 nipkow Linear arithmetic now copes with mixed nat/int formulae.
Tue, 25 Jul 2000 00:06:46 +0200 wenzelm rearranged setup of arithmetic procedures, avoiding global reference values;
less more (0) tip