| Mon, 12 Jan 2004 16:45:35 +0100 | paulson | Modified real arithmetic simplification | file | diff | annotate |
| Tue, 06 Jan 2004 10:40:15 +0100 | paulson | Ring_and_Field now requires axiom add_left_imp_eq for semirings. | file | diff | annotate |
| Thu, 01 Jan 2004 10:06:32 +0100 | paulson | tweaking of lemmas in RealDef, RealOrd | file | diff | annotate |
| Fri, 21 Nov 2003 11:15:40 +0100 | paulson | HOL: installation of Ring_and_Field as the basis for Naturals and Reals | file | diff | annotate |
| Thu, 20 Nov 2003 10:41:39 +0100 | paulson | including 0 ~= 1 in definition of Field | file | diff | annotate |
| Sun, 13 Jan 2002 21:14:31 +0100 | wenzelm | tuned; | file | diff | annotate |
| Sun, 13 Jan 2002 19:42:30 +0100 | wenzelm | Real/Complex_Numbers.thy; | file | diff | annotate |