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-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-06 blanchet 2010-08-06 quotient types registered as codatatypes are no longer quotient types
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05 blanchet 2010-08-05 fiddle with specialization etc.
2010-08-05 blanchet 2010-08-05 handle inductive predicates correctly after change in "def" semantics
2010-08-05 blanchet 2010-08-05 don't specialize built-ins or constructors
2010-08-05 blanchet 2010-08-05 prevent the expansion of too large definitions -- use equations for these instead
2010-08-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 blanchet 2010-08-03 handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-02 blanchet 2010-08-02 fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02 blanchet 2010-08-02 prevent generation of needless specialized constants etc.
2010-07-21 blanchet 2010-07-21 do a better job at Skolemizing in Nitpick, for TPTP FOF
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-21 blanchet 2010-06-21 optimized code generated for datatype cases + more; more = lazy creation of debugging messages in mono code + use of "let" when performing some beta-applications (to avoid exponential blowup) + removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)
2010-06-01 blanchet 2010-06-01 fix Nitpick soundness bug regarding The and Eps
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-05-31 blanchet 2010-05-31 don't include any axioms for "TYPE" in Nitpick
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-25 blanchet 2010-04-25 remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-24 blanchet 2010-04-24 removed Nitpick's "uncurry" option
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-24 blanchet 2010-04-24 cosmetics
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-09 blanchet 2010-03-09 more work on Nitpick's finite sets
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
2010-02-25 blanchet 2010-02-25 improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type
2010-02-25 blanchet 2010-02-25 cosmetics
2010-02-23 blanchet 2010-02-23 improved precision of small sets in Nitpick
2010-02-23 blanchet 2010-02-23 improved Nitpick's support for quotient types
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-22 blanchet 2010-02-22 fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-18 blanchet 2010-02-18 added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-17 blanchet 2010-02-17 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17 blanchet 2010-02-17 don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-09 blanchet 2010-02-09 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
2010-02-04 blanchet 2010-02-04 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come