Fri, 05 Mar 2004 15:18:59 +0100 |
paulson |
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
|
file |
diff |
annotate
|
Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
Thu, 29 Jan 2004 16:51:17 +0100 |
paulson |
simplifications in the hyperreals
|
file |
diff |
annotate
|
Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
Wed, 14 Jan 2004 00:13:04 +0100 |
nipkow |
Told linear arithmetic package about injections "real" from nat/int into real.
|
file |
diff |
annotate
|
Mon, 12 Jan 2004 16:45:35 +0100 |
paulson |
Modified real arithmetic simplification
|
file |
diff |
annotate
|
Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
Sat, 03 Jan 2004 16:09:39 +0100 |
paulson |
Deleting more redundant theorems
|
file |
diff |
annotate
|
Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
Tue, 23 Dec 2003 16:52:49 +0100 |
paulson |
deleting redundant theorems
|
file |
diff |
annotate
|
Mon, 22 Dec 2003 12:50:22 +0100 |
paulson |
moving HyperArith0.ML to other theories
|
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
|
Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
Sun, 07 Dec 2003 16:30:06 +0100 |
paulson |
re-organisation of Real/RealArith0.ML; more `Isar scripts
|
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
|
Tue, 02 Dec 2003 11:48:15 +0100 |
paulson |
More re-organising of numerical theorems
|
file |
diff |
annotate
|
Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
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
|
Mon, 05 May 2003 18:23:40 +0200 |
paulson |
New material on integration, etc. Moving Hyperreal/ex
|
file |
diff |
annotate
|
Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
Mon, 29 Apr 2002 11:29:54 +0200 |
nipkow |
Had to update proof for some strange reason
|
file |
diff |
annotate
|
Thu, 13 Dec 2001 15:45:03 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
Wed, 12 Dec 2001 19:21:02 +0100 |
nipkow |
mods due to reorienting and renaming of real_minus_mult_eq1/2
|
file |
diff |
annotate
|
Thu, 29 Nov 2001 19:03:03 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|