| Thu, 17 Aug 2000 18:31:12 +0200 |
nipkow |
installed recdef congs data
|
changeset |
files
|
| Thu, 17 Aug 2000 18:30:48 +0200 |
nipkow |
added map_cong to recdef
|
changeset |
files
|
| Thu, 17 Aug 2000 16:23:50 +0200 |
wenzelm |
removed Lambda/Type.ML;
|
changeset |
files
|
| Thu, 17 Aug 2000 12:02:01 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
| Thu, 17 Aug 2000 12:01:09 +0200 |
paulson |
fixed a proof that had stopped working ???
|
changeset |
files
|
| Thu, 17 Aug 2000 12:00:23 +0200 |
paulson |
tidied & updated proofs, deleting some unused ones
|
changeset |
files
|
| Thu, 17 Aug 2000 11:56:47 +0200 |
paulson |
modified proofs: better rules for cancellation of common factors across comparisons
|
changeset |
files
|
| Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
changeset |
files
|
| Thu, 17 Aug 2000 10:42:57 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 17 Aug 2000 10:40:31 +0200 |
wenzelm |
cases: opaque by default;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:39:44 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
| Thu, 17 Aug 2000 10:39:30 +0200 |
wenzelm |
tuned error handling;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:39:12 +0200 |
wenzelm |
added 'symmetric' attribute;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:38:43 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:38:20 +0200 |
wenzelm |
sel_upd proc: include 'more' pseudo-field;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:37:33 +0200 |
wenzelm |
renamed 'mk_cases_tac' to 'ind_cases';
|
changeset |
files
|
| Thu, 17 Aug 2000 10:37:04 +0200 |
wenzelm |
changed 'opaque' option to 'open' (opaque is default);
|
changeset |
files
|
| Thu, 17 Aug 2000 10:35:49 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
| Thu, 17 Aug 2000 10:34:52 +0200 |
wenzelm |
converted to new-style theory;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:34:28 +0200 |
wenzelm |
done;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:34:11 +0200 |
wenzelm |
'symmetric' attribute;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:33:37 +0200 |
wenzelm |
fixed deps;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:33:13 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
| Thu, 17 Aug 2000 10:32:44 +0200 |
wenzelm |
index tokens;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:32:20 +0200 |
wenzelm |
cases/induct method: 'opaque' by default; added 'open' option;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:31:43 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 17 Aug 2000 10:31:10 +0200 |
wenzelm |
renamed 'RS' to 'THEN';
|
changeset |
files
|
| Thu, 17 Aug 2000 10:29:50 +0200 |
wenzelm |
fixed lbrace, rbrace;
|
changeset |
files
|