2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-27 krauss 2011-03-27 avoid *** in normal output, which usually marks errors in logs
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2010-11-26 wenzelm 2010-11-26 explicit use of unprefix;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-01 haftmann 2010-10-01 chop_while replace drop_while and take_while
2010-09-30 haftmann 2010-09-30 take_while, drop_while
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
2010-09-03 wenzelm 2010-09-03 prefer regular Proof.context over background theory; misc tuning and simplification;
2010-09-02 wenzelm 2010-09-02 just one refute.ML;
2010-09-02 wenzelm 2010-09-02 use existing Integer.pow, despite its slightly odd argument order;
2010-09-02 wenzelm 2010-09-02 tuned whitespace and indentation, emphasizing the logical structure of this long text;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 use HOLogic.boolT and @{typ bool} more pervasively
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-28 haftmann 2010-06-28 avoid List.all
2010-06-11 haftmann 2010-06-11 avoid references to old constdefs
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-31 blanchet 2010-05-31 move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver
2010-05-25 wenzelm 2010-05-25 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-05 haftmann 2010-05-05 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 blanchet 2010-04-29 expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute
2010-04-23 blanchet 2010-04-23 remove debugging code
2010-04-13 blanchet 2010-04-13 commented out unsound "lfp"/"gfp" handling + fixed set output syntax; the "lfp"/"gfp" bug can be reproduced by looking for a counterexample to lemma "(A \<union> B)^+ = A^+ \<union> B^+" Refute incorrectly finds a countermodel for cardinality 1 (the smallest counterexample requires cardinality 2).
2010-03-13 wenzelm 2010-03-13 more antiquotations;
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-12-14 blanchet 2009-12-14 added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections
2009-12-07 blanchet 2009-12-07 better error message in Refute when specifying a non-existing SAT solver
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-27 wenzelm 2009-10-27 normalized basic type abbreviations;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 blanchet 2009-10-21 merged
2009-10-21 blanchet 2009-10-21 fixed the "expect" mechanism of Refute in the face of timeouts
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-10-15 wenzelm 2009-10-15 normalized aliases of Output operations;
2009-10-02 wenzelm 2009-10-02 Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics); command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;