src/HOL/Tools/prop_logic.ML
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 21 May 2009 15:25:26 +0100 webertj implementation of definitional CNF improved
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
Thu, 31 Aug 2006 02:59:08 +0200 webertj term_of_prop_formula added
Sun, 09 Oct 2005 17:06:03 +0200 webertj Tactics sat and satx reimplemented, several improvements
Tue, 26 Jul 2005 14:14:13 +0200 webertj comment modified
Mon, 25 Jul 2005 21:40:43 +0200 webertj defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
Mon, 25 Jul 2005 15:51:30 +0200 webertj defcnf modified to internally use a reference
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Wed, 23 Feb 2005 15:00:03 +0100 webertj exception SAME removed
Fri, 19 Nov 2004 17:52:07 +0100 webertj comment modified
Thu, 17 Jun 2004 21:58:51 +0200 webertj improved defcnf conversion
Sun, 13 Jun 2004 17:57:35 +0200 webertj faster defcnf conversion
Mon, 17 May 2004 14:05:06 +0200 webertj Comments fixed
Wed, 28 Apr 2004 10:45:35 +0200 webertj comments modified
Wed, 10 Mar 2004 20:27:56 +0100 webertj Formulas of propositional logic
less more (0) tip