src/HOL/Tools/Nitpick/nitpick_mono.ML
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-05-04 blanchet 2014-05-04 tuned structure name
2014-05-04 blanchet 2014-05-04 renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
2014-05-04 boehmes 2014-05-04 removed obsolete internal SAT solvers
2014-05-01 boehmes 2014-05-01 added internal proof-producing SAT solver
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-14 wenzelm 2014-03-14 prefer more robust Synchronized.var;
2014-03-03 blanchet 2014-03-03 tuned ML names
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2014-02-20 wenzelm 2014-02-20 prefer cat_lines;
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-01-03 blanchet 2012-01-03 fixed a few more bugs in \Nitpick's new "set" support
2012-01-03 blanchet 2012-01-03 port part of Nitpick to "set" type constructor
2012-01-03 blanchet 2012-01-03 ported mono calculus to handle "set" type constructors
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2010-12-11 krauss 2010-12-11 made smlnj happy
2010-12-07 blanchet 2010-12-07 simplify monotonicity code after killing "fin_fun" optimization
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07 blanchet 2010-12-07 updated monotonicity calculus w.r.t. set products
2010-12-07 blanchet 2010-12-07 removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
2010-12-06 blanchet 2010-12-06 fix monotonicity type of None
2010-12-06 blanchet 2010-12-06 compile
2010-12-06 blanchet 2010-12-06 introduced hack to exploit the symmetry of equality in monotonicity calculus
2010-12-06 blanchet 2010-12-06 add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
2010-12-06 blanchet 2010-12-06 fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
2010-12-06 blanchet 2010-12-06 improve precision of forall in constancy part of the monotonicity calculus
2010-12-06 blanchet 2010-12-06 added some missing well-annotatedness constraints to monotonicity calculus
2010-12-06 blanchet 2010-12-06 improve precision of finite functions in monotonicity calculus
2010-12-06 blanchet 2010-12-06 use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
2010-12-06 blanchet 2010-12-06 fixed quantifier handling of new monotonicity calculus
2010-12-06 blanchet 2010-12-06 tune parentheses and indentation
2010-12-06 blanchet 2010-12-06 proper handling of frames for connectives in monotonicity calculus
2010-12-06 blanchet 2010-12-06 tune indentation
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