| Thu, 29 Jun 2000 22:35:45 +0200 |
wenzelm |
* formal comments (text blocks etc.) in new-style theories may now
|
changeset |
files
|
| Thu, 29 Jun 2000 22:32:45 +0200 |
wenzelm |
added method_setup;
|
changeset |
files
|
| Thu, 29 Jun 2000 22:32:08 +0200 |
wenzelm |
facts: handle multiple lists of arguments;
|
changeset |
files
|
| Thu, 29 Jun 2000 22:31:53 +0200 |
wenzelm |
fixed is_semicolon (keyword instead of command!);
|
changeset |
files
|
| Thu, 29 Jun 2000 22:31:29 +0200 |
wenzelm |
added add_method;
|
changeset |
files
|
| Thu, 29 Jun 2000 22:31:12 +0200 |
wenzelm |
have_theorems etc.: handle multiple lists of arguments;
|
changeset |
files
|
| Thu, 29 Jun 2000 22:29:46 +0200 |
wenzelm |
have_thmss: handle multiple lists of arguments;
|
changeset |
files
|
| Thu, 29 Jun 2000 16:50:52 +0200 |
paulson |
now freezes Vars in order to prevent errors in cases like these:
|
changeset |
files
|
| Thu, 29 Jun 2000 12:19:27 +0200 |
paulson |
tidied proofs using default rule equalityCE
|
changeset |
files
|
| Thu, 29 Jun 2000 12:17:18 +0200 |
paulson |
the default equalityCE simplifies proofs
|
changeset |
files
|
| Thu, 29 Jun 2000 12:16:43 +0200 |
paulson |
tidied
|
changeset |
files
|
| Thu, 29 Jun 2000 12:15:08 +0200 |
paulson |
fixed proof to cope with the default of equalityCE instead of equalityE
|
changeset |
files
|