src/HOL/Nitpick_Examples/Mono_Nits.thy
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-03 wenzelm 2015-07-03 tuned signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-04-03 blanchet 2014-04-03 removed clone (cf. 300f613060b0)
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2013-12-20 blanchet 2013-12-20 compile
2013-02-25 wenzelm 2013-02-25 prefer stateless 'ML_val' for tests;
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-01-03 blanchet 2012-01-03 reintroduced failing examples now that they work again, after reintroduction of "set"
2011-12-24 haftmann 2011-12-24 commented out examples which choke on strict set/pred distinction
2011-12-01 blanchet 2011-12-01 minor example tweak
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-02-21 blanchet 2011-02-21 adjust example
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-01-12 wenzelm 2011-01-12 compile;
2011-01-12 wenzelm 2011-01-12 reraise interrupts as usual;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-07 blanchet 2010-12-07 simplify monotonicity code after killing "fin_fun" optimization
2010-12-06 blanchet 2010-12-06 cleanup example
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 improve precision of forall in constancy part of the monotonicity calculus
2010-12-06 blanchet 2010-12-06 more work on the monotonicity evaluation driver
2010-12-06 blanchet 2010-12-06 added ML code for testing entire theories for monotonicity
2010-12-06 blanchet 2010-12-06 added examples to exercise new monotonicity code
2010-12-06 blanchet 2010-12-06 tuning
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-08-05 blanchet 2010-08-05 added record field
2010-06-21 blanchet 2010-06-21 adjusted Nitpick examples to latest changes + make them slightly faster
2010-06-01 blanchet 2010-06-01 adapt example
2010-04-25 blanchet 2010-04-25 remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-03-17 blanchet 2010-03-17 solve error in "Nitpick_Mono" + short path when no finite functions are inferred
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
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-24 blanchet 2010-02-24 make example compile
2010-02-17 blanchet 2010-02-17 fix example to reflect change in function signature
2010-02-05 blanchet 2010-02-05 added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
2010-02-04 blanchet 2010-02-04 adapted example following previous Nitpick change and fixed minor optimization in Nitpick
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
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-11-15 wenzelm 2009-11-15 provide actual Nitpick_HOL.extended_context;
2009-10-29 blanchet 2009-10-29 rename "NitpickMono" to "Nitpick_Mono" in example
2009-10-27 blanchet 2009-10-27 internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.