| Fri, 16 Jun 2000 13:33:39 +0200 | paulson | uncommented the last 2 examples; tidied | file | diff | annotate |
| Thu, 23 Sep 1999 18:39:05 +0200 | paulson | Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or | file | diff | annotate |
| Wed, 22 Sep 1999 21:04:34 +0200 | wenzelm | proper theory setup for Real/ex/BinEx; | file | diff | annotate |
| Mon, 30 Aug 1999 15:25:16 +0200 | paulson | new directory HOL/Real/ex of real examples | file | diff | annotate |