| Thu, 14 Dec 2000 19:36:48 +0100 |
wenzelm |
added Summation;
|
changeset |
files
|
| Thu, 14 Dec 2000 10:30:45 +0100 |
paulson |
many new proofs; still needs tidying
|
changeset |
files
|
| Thu, 14 Dec 2000 10:30:11 +0100 |
paulson |
new theorem real_lbound_gt_zero
|
changeset |
files
|
| Wed, 13 Dec 2000 17:46:49 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 13 Dec 2000 17:43:33 +0100 |
wenzelm |
eliminated GOAL syntax;
|
changeset |
files
|
| Wed, 13 Dec 2000 17:41:10 +0100 |
wenzelm |
fixed add_term_names: NameSpace.base;
|
changeset |
files
|
| Wed, 13 Dec 2000 16:22:10 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 13 Dec 2000 16:21:40 +0100 |
wenzelm |
* print modes "brackets" and "no_brackets" control output of nested =>
|
changeset |
files
|
| Wed, 13 Dec 2000 12:47:15 +0100 |
paulson |
tidying
|
changeset |
files
|
| Wed, 13 Dec 2000 12:46:47 +0100 |
paulson |
new material, including default simprules that should be introduced earlier
|
changeset |
files
|
| Wed, 13 Dec 2000 11:24:48 +0100 |
kleing |
fixed iter_wf proof
|
changeset |
files
|
| Wed, 13 Dec 2000 10:34:45 +0100 |
paulson |
another round of tidying-up
|
changeset |
files
|
| Wed, 13 Dec 2000 10:34:31 +0100 |
paulson |
working proofs up to isCont_has_Ub
|
changeset |
files
|
| Wed, 13 Dec 2000 10:31:46 +0100 |
paulson |
tidying and replacement of "integer" rules by "order" ones
|
changeset |
files
|
| Wed, 13 Dec 2000 10:31:08 +0100 |
kleing |
removed sorry proof
|
changeset |
files
|
| Wed, 13 Dec 2000 10:30:40 +0100 |
paulson |
tries harder to remove negative literals, e.g.
|
changeset |
files
|
| Wed, 13 Dec 2000 10:11:13 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 13 Dec 2000 09:39:53 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 13 Dec 2000 09:32:55 +0100 |
nipkow |
small mods.
|
changeset |
files
|
| Wed, 13 Dec 2000 09:30:59 +0100 |
nipkow |
sar split method uses new gen_split_tac.
|
changeset |
files
|
| Tue, 12 Dec 2000 14:08:48 +0100 |
kleing |
completeness (unfinished)
|
changeset |
files
|
| Tue, 12 Dec 2000 14:08:26 +0100 |
kleing |
added direction dynamic ==> static
|
changeset |
files
|
| Tue, 12 Dec 2000 14:07:11 +0100 |
kleing |
eliminated some warnings, tuned
|
changeset |
files
|
| Tue, 12 Dec 2000 12:01:19 +0100 |
paulson |
first stage in tidying up Real and Hyperreal.
|
changeset |
files
|