nipkow [Wed, 03 Dec 1997 17:25:43 +0100] rev 4356
Replaced n ~= 0 by 0 < n
wenzelm [Wed, 03 Dec 1997 12:55:04 +0100] rev 4355
pass return code!!
paulson [Wed, 03 Dec 1997 11:42:45 +0100] rev 4354
Fixed the treatment of substitution for equations, restricting occurrences of
variables on the RHS. Improves performance in many cases, though a few old
proofs fail
paulson [Wed, 03 Dec 1997 11:00:24 +0100] rev 4353
updated for latest Blast_tac, which treats equality differently
paulson [Wed, 03 Dec 1997 10:52:17 +0100] rev 4352
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson [Wed, 03 Dec 1997 10:50:02 +0100] rev 4351
Tidying and some comments
paulson [Wed, 03 Dec 1997 10:49:33 +0100] rev 4350
updated for latest Blast_tac, which treats equality differently
paulson [Wed, 03 Dec 1997 10:48:16 +0100] rev 4349
Instantiated the one-point-rule quantifier simpprocs for FOL
New file fologic.ML holds abstract syntax operations
Also, miniscoping provided for intuitionistic logic
paulson [Wed, 03 Dec 1997 10:47:13 +0100] rev 4348
updated for latest Blast_tac, which fixes an equality bug
paulson [Wed, 03 Dec 1997 10:45:42 +0100] rev 4347
Miniscoping now used except for one proof
wenzelm [Tue, 02 Dec 1997 12:42:59 +0100] rev 4346
adapted to new term order;
wenzelm [Tue, 02 Dec 1997 12:42:28 +0100] rev 4345
tuned term order;
added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;
wenzelm [Tue, 02 Dec 1997 12:41:29 +0100] rev 4344
tuned trfuns types;
wenzelm [Tue, 02 Dec 1997 12:41:02 +0100] rev 4343
added prod_ord, dict_ord, list_ord;