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 |