src/HOL/Tools/refute.ML
2006-11-09 webertj 2006-11-09 interpreters for fst and snd added
2006-10-23 haftmann 2006-10-23 switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15 webertj 2006-09-15 trivial whitespace change
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_term;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-02-06 wenzelm 2006-02-06 Logic.const_of_class/class_of_const;
2006-01-23 webertj 2006-01-23 TimeLimit replaced by interrupt_timeout
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-09-19 webertj 2005-09-19 SAT solver interface modified to support proofs of unsatisfiability
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c";
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-07-28 wenzelm 2005-07-28 Sign.typ_match;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-06-11 wenzelm 2005-06-11 accomodate changed #classes;
2005-06-09 wenzelm 2005-06-09 Theory.all_axioms_of;
2005-06-03 webertj 2005-06-03 fixed a typo in the gfp interpreter
2005-05-25 paulson 2005-05-25 SML/NJ compatibility
2005-05-23 webertj 2005-05-23 interpreters for lfp/gfp added
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-20 webertj 2005-04-20 call to Array.modifyi replaced
2005-04-19 webertj 2005-04-19 compilation error fixed
2005-04-18 webertj 2005-04-18 support for recursion over mutually recursive IDTs
2005-03-17 webertj 2005-03-17 Bugfix related to the interpretation of IDT constructors
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 webertj 2005-03-03 interpreter for Finite_Set.Finites added
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-23 webertj 2005-02-23 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 skalberg 2005-02-13 Deleted Library.option type.
2004-11-25 webertj 2004-11-25 minor code refactoring (typ_of_dtyp, size_of_dtyp)
2004-11-25 webertj 2004-11-25 exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
2004-11-25 webertj 2004-11-25 comments edited
2004-11-17 webertj 2004-11-17 minor changes (comments/code refactoring)
2004-11-14 webertj 2004-11-14 DOCTYPE declaration added
2004-11-12 webertj 2004-11-12 minor code refactoring
2004-08-09 webertj 2004-08-09 warning for recursion over IDTs added
2004-06-21 wenzelm 2004-06-21 immediate_output;
2004-06-17 webertj 2004-06-17 new SAT solver interface
2004-05-29 wenzelm 2004-05-29 Output.output;
2004-05-26 webertj 2004-05-26 adjusted for different signature of Type.typ_instance
2004-05-26 webertj 2004-05-26 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 webertj 2004-04-16 exactly1true rewritten (much better when converting to CNF now)
2004-03-26 webertj 2004-03-26 slightly different SAT solver interface
2004-03-11 webertj 2004-03-11 SML/NJ compatibility fixes
2004-03-10 webertj 2004-03-10 support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
2004-01-12 webertj 2004-01-12 Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.