src/HOL/Tools/prop_logic.ML
Wed, 14 Mar 2007 01:35:02 +0100 webertj is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
less more (0) -10 -1 tip