| 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
|
| Wed, 22 Mar 2000 12:33:34 +0100 |
paulson |
new meta-rule "inst", a shorthand for read_instantiate_sg
|
changeset |
files
|
| Tue, 21 Mar 2000 17:43:54 +0100 |
wenzelm |
goal_spec: [!];
|
changeset |
files
|
| Tue, 21 Mar 2000 17:32:44 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Mar 2000 17:32:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Mar 2000 15:32:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Mar 2000 15:26:21 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Tue, 21 Mar 2000 15:23:33 +0100 |
wenzelm |
help message;
|
changeset |
files
|