| Fri, 24 Mar 2000 11:52:19 +0100 |
wenzelm |
-o sty;
|
changeset |
files
|
| Fri, 24 Mar 2000 08:56:48 +0100 |
nipkow |
comments
|
changeset |
files
|
| Thu, 23 Mar 2000 21:37:13 +0100 |
wenzelm |
added 'moreover' command;
|
changeset |
files
|
| Thu, 23 Mar 2000 21:36:43 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Thu, 23 Mar 2000 11:28:10 +0100 |
wenzelm |
tuned spacing;
|
changeset |
files
|
| Thu, 23 Mar 2000 11:27:52 +0100 |
wenzelm |
ex/Antiquote.thy made new-style theory;
|
changeset |
files
|
| Thu, 23 Mar 2000 10:23:54 +0100 |
paulson |
now exclusively uses rtac/dtac/etac rather than the long forms
|
changeset |
files
|
| Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
changeset |
files
|
| Wed, 22 Mar 2000 13:23:57 +0100 |
paulson |
made a proof more robust (did not like Suc_less_eq)
|
changeset |
files
|
| Wed, 22 Mar 2000 13:22:39 +0100 |
paulson |
Suc_less_eq now with AddIffs. How could this have been overlooked?
|
changeset |
files
|
| Wed, 22 Mar 2000 13:22:11 +0100 |
paulson |
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
|
changeset |
files
|
| Wed, 22 Mar 2000 13:01:57 +0100 |
paulson |
made more robust
|
changeset |
files
|
| Wed, 22 Mar 2000 13:01:18 +0100 |
paulson |
tidied using new "inst" rule
|
changeset |
files
|
| Wed, 22 Mar 2000 12:45:41 +0100 |
paulson |
tidied using new "inst" rule
|
changeset |
files
|