| Wed, 03 Dec 1997 10:52:17 +0100 |
paulson |
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
|
changeset |
files
|
| Wed, 03 Dec 1997 10:50:02 +0100 |
paulson |
Tidying and some comments
|
changeset |
files
|
| Wed, 03 Dec 1997 10:49:33 +0100 |
paulson |
updated for latest Blast_tac, which treats equality differently
|
changeset |
files
|
| Wed, 03 Dec 1997 10:48:16 +0100 |
paulson |
Instantiated the one-point-rule quantifier simpprocs for FOL
|
changeset |
files
|
| Wed, 03 Dec 1997 10:47:13 +0100 |
paulson |
updated for latest Blast_tac, which fixes an equality bug
|
changeset |
files
|
| Wed, 03 Dec 1997 10:45:42 +0100 |
paulson |
Miniscoping now used except for one proof
|
changeset |
files
|
| Tue, 02 Dec 1997 12:42:59 +0100 |
wenzelm |
adapted to new term order;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:42:28 +0100 |
wenzelm |
tuned term order;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:41:29 +0100 |
wenzelm |
tuned trfuns types;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:41:02 +0100 |
wenzelm |
added prod_ord, dict_ord, list_ord;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:40:06 +0100 |
wenzelm |
File.tmp_name;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:39:03 +0100 |
wenzelm |
added tmp_name;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:38:39 +0100 |
wenzelm |
ISABELLE_TMP;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:38:08 +0100 |
wenzelm |
added context.ML;
|
changeset |
files
|
| Tue, 02 Dec 1997 12:37:44 +0100 |
wenzelm |
Global contexts: session and theory.
|
changeset |
files
|