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;