src/HOL/Nitpick.thy
2015-09-06 wenzelm 2015-09-06 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-15 blanchet 2014-09-15 generate 'code' attribute only if 'code' plugin is enabled
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-08-19 blanchet 2014-08-19 tuning
2014-06-12 blanchet 2014-06-12 tuned dependencies
2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-31 blanchet 2014-01-31 tuned ML file name
2014-01-20 blanchet 2014-01-20 compile
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2013-11-21 blanchet 2013-11-21 rationalize imports
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2012-10-31 blanchet 2012-10-31 moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-24 wenzelm 2012-05-24 tuned proofs;
2012-05-11 blanchet 2012-05-11 fixed "real" after they were redefined as a 'quotient_type'
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-01-23 blanchet 2012-01-23 added problem importer
2012-01-23 blanchet 2012-01-23 rebranded Nitrox, for more uniformity
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-10-13 haftmann 2011-10-13 bouned transitive closure
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-08-02 krauss 2011-08-02 replaced Nitpick's hardwired basic_ersatz_table by context data
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-03-22 blanchet 2011-03-22 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
2011-02-21 blanchet 2011-02-21 rename Nitpick's (internal) auxiliary lemmas
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
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 fix special handling of set products
2010-09-14 blanchet 2010-09-14 remove more clutter related to old "fast_descrs" optimization
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-08 blanchet 2010-09-08 merge
2010-09-06 blanchet 2010-09-06 remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-12 haftmann 2010-08-12 group record-related ML files
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-06-11 blanchet 2010-06-11 adjust Nitpick's handling of "<" on "rat"s and "reals"
2010-05-31 blanchet 2010-05-31 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-14 blanchet 2010-05-14 add "no_atp"s to Nitpick lemmas
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-10 blanchet 2010-03-10 improve precision of "card" in Nitpick
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-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-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-13 blanchet 2010-02-13 more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-12 blanchet 2010-02-12 various cosmetic changes to Nitpick