Wed, 28 Jan 2004 17:01:01 +0100 |
paulson |
tidying up arithmetic for the hyperreals
|
file |
diff |
annotate
|
Wed, 28 Jan 2004 10:41:49 +0100 |
paulson |
converted Real/Lubs to Isar script. Converting arithmetic setup
|
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 04:41:16 +0100 |
nipkow |
fixed old bugs in "decomp" (conversion from term to lin.arith. format).
|
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
|
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
|
Tue, 23 Dec 2003 14:46:08 +0100 |
paulson |
new theorems
|
file |
diff |
annotate
|
Tue, 23 Dec 2003 12:54:15 +0100 |
paulson |
more ML bindings
|
file |
diff |
annotate
|
Mon, 22 Dec 2003 15:41:25 +0100 |
paulson |
new binding
|
file |
diff |
annotate
|
Mon, 22 Dec 2003 12:50:01 +0100 |
paulson |
removing obsolete bindings
|
file |
diff |
annotate
|
Fri, 19 Dec 2003 17:13:28 +0100 |
paulson |
tidying first part of HyperArith0.ML, using generic lemmas
|
file |
diff |
annotate
|
Fri, 12 Dec 2003 15:05:18 +0100 |
paulson |
moving some division theorems to Ring_and_Field
|
file |
diff |
annotate
|
Wed, 10 Dec 2003 16:47:50 +0100 |
paulson |
combining Real/{RealArith0,real_arith}.ML
|
file |
diff |
annotate
|
Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
Mon, 01 Jan 2001 11:52:04 +0100 |
paulson |
minor tidying of simprocs
|
file |
diff |
annotate
|
Thu, 21 Dec 2000 18:57:12 +0100 |
nipkow |
rational linear arithmetic
|
file |
diff |
annotate
|
Mon, 18 Dec 2000 14:59:05 +0100 |
nipkow |
moved mk_bin from Numerals to HOLogic
|
file |
diff |
annotate
|
Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|