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;
wenzelm [Tue, 02 Dec 1997 12:40:06 +0100] rev 4342
File.tmp_name;
wenzelm [Tue, 02 Dec 1997 12:39:03 +0100] rev 4341
added tmp_name;