Thu, 01 Jan 2004 10:06:32 +0100 | paulson | tweaking of lemmas in RealDef, RealOrd | file | diff | annotate |
Thu, 25 Dec 2003 22:48:32 +0100 | paulson | re-organized some hyperreal and real lemmas | file | diff | annotate |
Fri, 19 Dec 2003 17:13:28 +0100 | paulson | tidying first part of HyperArith0.ML, using generic lemmas | file | diff | annotate |
Sat, 13 Dec 2003 09:33:52 +0100 | paulson | absolute value theorems moved to HOL/Ring_and_Field | file | diff | annotate |
Fri, 05 Dec 2003 18:10:59 +0100 | paulson | more field division lemmas transferred from Real to Ring_and_Field | file | diff | annotate |
Mon, 05 May 2003 18:23:40 +0200 | paulson | New material on integration, etc. Moving Hyperreal/ex | file | diff | annotate |