Fri, 18 Nov 2005 07:06:07 +0100 mengj -- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
Fri, 18 Nov 2005 07:05:11 +0100 mengj -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
Wed, 16 Nov 2005 19:34:19 +0100 wenzelm tuned document;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip