src/HOL/Tools/refute.ML
2009-02-06 blanchet 2009-02-06 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
2009-02-04 blanchet 2009-02-04 Make some Refute functions public so I can use them in Nitpick, use @{const_name} antiquotation whenever possible (some, like Lfp.lfp had been renamed since Tjark wrote Refute), and removed some "set"-related code that is no longer relevant in Isabelle2008. There's still some "set" code that needs to be ported; see TODO in the file.
2009-01-01 wenzelm 2009-01-01 avoid polymorphic equality;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-10-15 webertj 2007-10-15 interpreter for List.append added again
2007-10-12 webertj 2007-10-12 significant code overhaul, bugfix for inductive data types
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again);
2007-09-24 wenzelm 2007-09-24 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions;
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-01-19 webertj 2007-01-19 interpreter for Finite_Set.finite added
2007-01-19 webertj 2007-01-19 reformatted to 80 chars/line
2007-01-10 webertj 2007-01-10 tuned
2007-01-05 webertj 2007-01-05 reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
2007-01-04 webertj 2007-01-04 using Array.modifyi (no functional change)
2007-01-04 webertj 2007-01-04 obsolete sign_of calls removed
2007-01-04 webertj 2007-01-04 constants are unfolded, universal quantifiers are stripped, some minor changes
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-11-27 webertj 2006-11-27 outermost universal quantifiers are stripped
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