src/HOL/Nitpick.thy
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Mon, 05 Jun 2017 15:59:45 +0200 haftmann simplified setup
Sun, 23 Apr 2017 14:53:33 +0200 haftmann include GCD as integral part of computational algebra in session HOL
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Thu, 15 Sep 2016 11:48:20 +0200 nipkow renamed listsum -> sum_list, listprod ~> prod_list
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Sun, 15 Nov 2015 12:39:51 +0100 wenzelm option "inductive_defs" controls exposure of def and mono facts;
Sun, 06 Sep 2015 21:55:13 +0200 wenzelm do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Mon, 15 Sep 2014 10:49:07 +0200 blanchet generate 'code' attribute only if 'code' plugin is enabled
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Tue, 19 Aug 2014 09:34:41 +0200 blanchet tuning
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuned dependencies
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies
Wed, 23 Apr 2014 10:23:27 +0200 blanchet move size hooks together, with new one preceding old one and sharing same theory data
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Mon, 17 Feb 2014 22:54:38 +0100 blanchet simplified data structure by reducing the incidence of clumsy indices
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name
Mon, 20 Jan 2014 20:00:33 +0100 blanchet compile
Thu, 16 Jan 2014 16:20:17 +0100 blanchet adapted to move of Wfrec
Thu, 21 Nov 2013 21:33:34 +0100 blanchet rationalize imports
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 24 May 2012 17:25:53 +0200 wenzelm tuned proofs;
Fri, 11 May 2012 00:45:24 +0200 blanchet fixed "real" after they were redefined as a 'quotient_type'
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer
Mon, 23 Jan 2012 17:40:31 +0100 blanchet rebranded Nitrox, for more uniformity
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Thu, 13 Oct 2011 23:27:46 +0200 haftmann bouned transitive closure
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Tue, 02 Aug 2011 12:27:24 +0200 krauss replaced Nitpick's hardwired basic_ersatz_table by context data
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Tue, 22 Mar 2011 19:04:32 +0100 blanchet 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
Mon, 21 Feb 2011 11:50:38 +0100 blanchet rename Nitpick's (internal) auxiliary lemmas
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Tue, 07 Dec 2010 11:56:53 +0100 blanchet remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
Tue, 07 Dec 2010 11:56:01 +0100 blanchet fix special handling of set products
Tue, 14 Sep 2010 16:33:38 +0200 blanchet remove more clutter related to old "fast_descrs" optimization
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Wed, 08 Sep 2010 16:01:06 +0200 blanchet merge
Mon, 06 Sep 2010 17:51:26 +0200 blanchet remove "minipick" (the toy version of Nitpick) and some tests;
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 12 Aug 2010 17:56:41 +0200 haftmann group record-related ML files
Sat, 03 Jul 2010 00:50:35 +0200 blanchet adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
Fri, 11 Jun 2010 17:05:11 +0200 blanchet adjust Nitpick's handling of "<" on "rat"s and "reals"
less more (0) -60 tip