paulson [Tue, 20 Aug 1996 17:46:24 +0200] rev 1929
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson [Tue, 20 Aug 1996 12:40:17 +0200] rev 1928
Added ref to allow suppression of error msgs
paulson [Tue, 20 Aug 1996 12:39:30 +0200] rev 1927
New classical reasoner: warns of, and ignores, redundant rules.
Also warns of rules supplied with different "hints" (Safe, etc.)
paulson [Tue, 20 Aug 1996 12:36:58 +0200] rev 1926
Addition of function set_of_list
paulson [Tue, 20 Aug 1996 12:32:16 +0200] rev 1925
Some tidying. This brittle proof depends upon
AddSEs [less_SucE];
paulson [Tue, 20 Aug 1996 12:23:13 +0200] rev 1924
Corrected for new classical reasoner: redundant rules
are now ignored, even if this could increase their priority
nipkow [Mon, 19 Aug 1996 15:35:11 +0200] rev 1923
updated html-link
paulson [Mon, 19 Aug 1996 13:06:30 +0200] rev 1922
Installation of auto_tac; re-organization
paulson [Mon, 19 Aug 1996 13:03:17 +0200] rev 1921
Tidied up the proofs
paulson [Mon, 19 Aug 1996 11:51:39 +0200] rev 1920
Added impOfSubs