src/HOL/Tools/refute.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-29 ago expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-23 ago remove debugging code
2010-04-13 ago commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
2010-03-13 ago more antiquotations;
2010-02-19 ago moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 ago moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 ago new theory Algebras.thy for generic algebraic structures
2009-12-14 ago added "no_assms" option to Refute, and include structured proof assumptions by default;
2009-12-07 ago better error message in Refute when specifying a non-existing SAT solver
2009-11-30 ago modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-24 ago curried take/drop
2009-11-08 ago adapted Theory_Data;
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-27 ago eliminated some old folds;
2009-10-27 ago normalized basic type abbreviations;
2009-10-22 ago map_range (and map_index) combinator
2009-10-21 ago merged
2009-10-21 ago fixed the "expect" mechanism of Refute in the face of timeouts
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago merged
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 ago standardized basic operations on type option;
2009-10-19 ago uniform use of Integer.add/mult/sum/prod;
2009-10-15 ago replaced String.concat by implode;
2009-10-15 ago normalized aliases of Output operations;
2009-10-02 ago Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
2009-07-10 ago dropped find_index_eq
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-06-23 ago tuned interfaces of datatype module
2009-06-21 ago simplified names of common datatype types
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-11 ago HOLogic.mk_set, HOLogic.dest_set
2009-03-07 ago Added a second timeout mechanism to Refute.
2009-03-07 ago Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
2009-03-06 ago Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
2009-03-06 ago Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
2009-03-06 ago merged
2009-03-05 ago merged
2009-03-05 ago set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05 ago Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-04 ago Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-01 ago use long names for old-style fold combinators;
2009-02-17 ago Reintroduce set_interpreter for Collect and op :.
2009-02-06 ago Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
2009-02-04 ago Make some Refute functions public so I can use them in Nitpick,
2009-01-01 ago avoid polymorphic equality;
2008-12-31 ago use regular Term.add_XXX etc.;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 ago removed Table.extend, NameSpace.extend_table
2008-10-07 ago arbitrary is undefined
2008-05-18 ago eliminated theory CPure;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago cat_lines;
2008-03-27 ago removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-19 ago Type.lookup now curried