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;