Thu, 21 Dec 2000 18:53:32 +0100 |
paulson |
this makes the proof run (or run faster)
|
file |
diff |
annotate
|
Thu, 21 Dec 2000 18:08:10 +0100 |
paulson |
further tidying of NSA proofs
|
file |
diff |
annotate
|
Thu, 21 Dec 2000 10:16:33 +0100 |
paulson |
more tidying, especially to rationalize the simprules
|
file |
diff |
annotate
|
Wed, 20 Dec 2000 12:15:52 +0100 |
paulson |
further tidying
|
file |
diff |
annotate
|
Tue, 19 Dec 2000 15:06:59 +0100 |
paulson |
more tidying
|
file |
diff |
annotate
|
Fri, 15 Dec 2000 17:41:38 +0100 |
paulson |
further round of tidying
|
file |
diff |
annotate
|
Tue, 12 Dec 2000 12:01:19 +0100 |
paulson |
first stage in tidying up Real and Hyperreal.
|
file |
diff |
annotate
|
Wed, 06 Dec 2000 12:34:40 +0100 |
bauerg |
converted rinv and hrinv to inverse;
|
file |
diff |
annotate
|
Fri, 01 Dec 2000 11:02:55 +0100 |
paulson |
renamed less_eq_Suc_add to less_imp_Suc_add
|
file |
diff |
annotate
|
Thu, 21 Sep 2000 12:17:11 +0200 |
fleuriot |
New theories: construction of hypernaturals, nonstandard extensions,
|
file |
diff |
annotate
|