src/HOL/Tools/Nitpick/nitpick_mono.ML
2010-12-06 blanchet 2010-12-06 removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06 blanchet 2010-12-06 implemented All rules from new monotonicity calculus
2010-12-06 blanchet 2010-12-06 fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
2010-12-06 blanchet 2010-12-06 started implementing the new monotonicity rules for application
2010-12-06 blanchet 2010-12-06 implemented connectives in new monotonicity calculus
2010-12-06 blanchet 2010-12-06 added "Neq" operator to monotonicity inference module
2010-12-06 blanchet 2010-12-06 started implementing connectives in new monotonicity calculus
2010-12-06 blanchet 2010-12-06 more work on frames in the new monotonicity calculus
2010-12-06 blanchet 2010-12-06 support 3 monotonicity calculi in one and fix soundness bug
2010-12-06 blanchet 2010-12-06 proper handling of assignment disjunctions vs. conjunctions
2010-12-06 blanchet 2010-12-06 adapt monotonicity code to four annotation types
2010-12-06 blanchet 2010-12-06 more monotonicity tuning
2010-12-06 blanchet 2010-12-06 tuning
2010-12-06 blanchet 2010-12-06 added frame component to Gamma in monotonicity calculus
2010-12-06 blanchet 2010-12-06 use boolean pair to encode annotation, which may now take four values
2010-12-06 blanchet 2010-12-06 started generalizing monotonicity code to accommodate new calculus
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-10-26 blanchet 2010-10-26 whitespace tuning
2010-10-21 blanchet 2010-10-21 cosmetics
2010-09-14 blanchet 2010-09-14 eliminate more clutter related to "fast_descrs" optimization
2010-09-14 blanchet 2010-09-14 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound
2010-09-13 blanchet 2010-09-13 remove unreferenced identifiers
2010-09-13 blanchet 2010-09-13 correctly thread parameter through
2010-09-11 blanchet 2010-09-11 change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
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-05 blanchet 2010-08-05 deal correctly with Pure.conjunction in mono check
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 make tracing monotonicity easier
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 code that used to raise an exception if bound variables were given a finite function type, because the old vs. new bound variable types were confused
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-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-03-18 blanchet 2010-03-18 added type constraints to make SML/NJ happy
2010-03-17 blanchet 2010-03-17 solve error in "Nitpick_Mono" + short path when no finite functions are inferred
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-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-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-18 blanchet 2010-02-18 fix bug in Nitpick's monotonicity code w.r.t. binary integers
2010-02-17 blanchet 2010-02-17 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-04 blanchet 2010-02-04 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-04 blanchet 2010-02-04 four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 blanchet 2010-01-20 some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
2009-12-14 blanchet 2009-12-14 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick; this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on
2009-12-14 blanchet 2009-12-14 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
2009-12-04 blanchet 2009-12-04 fixed paths in Nitpick's ML file headers
2009-11-23 blanchet 2009-11-23 improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex
2009-11-16 blanchet 2009-11-16 added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus