src/HOL/Tools/prop_logic.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-05-21 webertj 2009-05-21 implementation of definitional CNF improved
2007-03-14 webertj 2007-03-14 is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
2006-08-31 webertj 2006-08-31 term_of_prop_formula added
2005-10-09 webertj 2005-10-09 Tactics sat and satx reimplemented, several improvements
2005-07-26 webertj 2005-07-26 comment modified
2005-07-25 webertj 2005-07-25 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
2005-07-25 webertj 2005-07-25 defcnf modified to internally use a reference
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-23 webertj 2005-02-23 exception SAME removed
2004-11-19 webertj 2004-11-19 comment modified
2004-06-17 webertj 2004-06-17 improved defcnf conversion
2004-06-13 webertj 2004-06-13 faster defcnf conversion
2004-05-17 webertj 2004-05-17 Comments fixed
2004-04-28 webertj 2004-04-28 comments modified
2004-03-10 webertj 2004-03-10 Formulas of propositional logic