paulson [Thu, 22 Feb 2007 10:25:14 +0100] rev 22345
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
are now returned, fixing a bug in the metis method.
krauss [Wed, 21 Feb 2007 13:51:12 +0100] rev 22344
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
to fail when the other term in the comparison was itself a bound variable,
as in "EX y. ALL x>=y. P x".
kleing [Wed, 21 Feb 2007 02:30:06 +0100] rev 22343
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
kleing [Tue, 20 Feb 2007 00:53:18 +0100] rev 22342
added missing \
kleing [Tue, 20 Feb 2007 00:23:58 +0100] rev 22341
updated docs with new with_dups syntax for find_theorems
kleing [Tue, 20 Feb 2007 00:14:33 +0100] rev 22340
Remove duplicates from printed theorems in find_theorems
(still pretty slow, needs optimising).
Added syntax "find_theorems (..) with_dups .." to switch off removal.