src/HOL/Tools/refute.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2005-09-19 ago SAT solver interface modified to support proofs of unsatisfiability
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-08 ago introduces some modern-style AList operations
2005-09-06 ago axclass: name space prefix is now "c_class" instead of just "c";
2005-09-05 ago curried_lookup/update;
2005-07-28 ago Sign.typ_match;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago accomodate changed #classes;
2005-06-09 ago Theory.all_axioms_of;
2005-06-03 ago fixed a typo in the gfp interpreter
2005-05-25 ago SML/NJ compatibility
2005-05-23 ago interpreters for lfp/gfp added
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-20 ago call to Array.modifyi replaced
2005-04-19 ago compilation error fixed
2005-04-18 ago support for recursion over mutually recursive IDTs
2005-03-17 ago Bugfix related to the interpretation of IDT constructors
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago interpreter for Finite_Set.Finites added
2005-03-03 ago Move towards standard functions.
2005-02-23 ago major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
2005-02-13 ago Deleted Library.option type.
2004-11-25 ago minor code refactoring (typ_of_dtyp, size_of_dtyp)
2004-11-25 ago exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
2004-11-25 ago comments edited
2004-11-17 ago minor changes (comments/code refactoring)
2004-11-14 ago DOCTYPE declaration added
2004-11-12 ago minor code refactoring
2004-08-09 ago warning for recursion over IDTs added
2004-06-21 ago immediate_output;
2004-06-17 ago new SAT solver interface
2004-05-29 ago Output.output;
2004-05-26 ago adjusted for different signature of Type.typ_instance
2004-05-26 ago major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
2004-04-16 ago exactly1true rewritten (much better when converting to CNF now)
2004-03-26 ago slightly different SAT solver interface
2004-03-11 ago SML/NJ compatibility fixes
2004-03-10 ago support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
2004-01-12 ago Fixed compatibility issues with SML/NJ:
2004-01-10 ago Adding 'refute' to HOL.