Wed, 13 Sep 2006 12:21:35 +0200 paulson Added the "theory_const" option. Only it is OFF because it's often harmful!
Wed, 13 Sep 2006 12:20:21 +0200 paulson Extended the blacklist with higher-order theorems. Restructured. Added checks to
Wed, 13 Sep 2006 12:18:36 +0200 paulson bug fix to abstractions: free variables in theorem can be abstracted over.
Wed, 13 Sep 2006 12:17:17 +0200 paulson Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
(0) -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip