Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_hol.ML
Sat, 24 Jan 2015 22:00:24 +0100 wenzelm tuned signature; file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list) file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; file | diff | annotate
Tue, 19 Aug 2014 09:34:41 +0200 blanchet tuning file | diff | annotate
Sat, 16 Aug 2014 22:14:57 +0200 wenzelm updated to named_theorems; file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet removed subsumed record-related code, now that records are registered as 'ctr_sugar' file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet made lookup more robust in the face of missing (dummy) case constant file | diff | annotate
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names; file | diff | annotate
Fri, 21 Mar 2014 12:34:50 +0100 wenzelm more qualified names; file | diff | annotate
Wed, 19 Mar 2014 22:10:33 +0100 wenzelm more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile); file | diff | annotate
Sat, 15 Mar 2014 11:59:18 +0100 wenzelm tuned signature; file | diff | annotate
Mon, 03 Mar 2014 23:05:30 +0100 blanchet fixed handling of 'case_prod' and other 'case' functions for interpreted types file | diff | annotate
Mon, 03 Mar 2014 22:33:22 +0100 blanchet support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's file | diff | annotate
Mon, 03 Mar 2014 22:33:22 +0100 blanchet tuned ML names file | diff | annotate
Mon, 03 Mar 2014 22:33:22 +0100 blanchet tuned code file | diff | annotate
Mon, 03 Mar 2014 22:33:22 +0100 blanchet removed nonstandard models from Nitpick file | diff | annotate
Mon, 03 Mar 2014 12:58:17 +0100 blanchet guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick file | diff | annotate
Wed, 19 Feb 2014 08:34:34 +0100 blanchet adapted Nitpick to 'primrec' refactoring file | diff | annotate
Mon, 17 Feb 2014 22:54:38 +0100 blanchet simplified data structure by reducing the incidence of clumsy indices file | diff | annotate
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...' file | diff | annotate
Mon, 20 Jan 2014 19:51:56 +0100 blanchet have Nitpick lookup codatatypes file | diff | annotate
Thu, 16 Jan 2014 16:20:17 +0100 blanchet adapted to move of Wfrec file | diff | annotate
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _) file | diff | annotate
Sun, 10 Nov 2013 10:02:34 +0100 haftmann dropped obsolete check: dest_num always yields positive number file | diff | annotate
Tue, 24 Sep 2013 11:02:42 +0200 blanchet encode goal digest in spying log (to detect duplicates) file | diff | annotate
Mon, 23 Sep 2013 18:40:02 +0200 blanchet don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it) file | diff | annotate
Tue, 28 May 2013 19:59:54 +0200 blanchet don't create needless constant file | diff | annotate
Mon, 15 Apr 2013 10:41:03 +0200 blanchet not all Nitpick 'constructors' are injective -- careful file | diff | annotate
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral; file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved Refute to "HOL/Library" to speed up building "Main" even more file | diff | annotate
Fri, 12 Oct 2012 15:08:29 +0200 wenzelm discontinued typedef with implicit set_def; file | diff | annotate
Wed, 15 Aug 2012 11:04:56 +0200 blanchet fixed handling of "int" in the wake of its port to the quotient package file | diff | annotate
Wed, 15 Aug 2012 11:04:55 +0200 blanchet removed dead code file | diff | annotate
Thu, 24 May 2012 17:46:35 +0200 blanchet fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality file | diff | annotate
Fri, 11 May 2012 00:45:24 +0200 blanchet fixed "real" after they were redefined as a 'quotient_type' file | diff | annotate
Thu, 26 Apr 2012 20:09:38 +0200 blanchet fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function file | diff | annotate
Sun, 22 Apr 2012 14:16:46 +0200 blanchet more meaningful default value file | diff | annotate
Sun, 22 Apr 2012 14:16:45 +0200 blanchet handle exception (needed to solve TPTP problem SEU880^5) file | diff | annotate
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow") file | diff | annotate
Mon, 26 Mar 2012 10:42:06 +0200 blanchet fixed Nitpick after numeral representation change (2a1953f0d20d) file | diff | annotate
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS) file | diff | annotate
Sun, 04 Mar 2012 23:20:43 +0100 blanchet addressed a quotient-type-related issue that arose with the port to "set" file | diff | annotate
Thu, 01 Mar 2012 11:28:56 +0100 blanchet improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case file | diff | annotate
Thu, 01 Mar 2012 11:28:56 +0100 blanchet fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate
Tue, 17 Jan 2012 18:25:36 +0100 blanchet fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick file | diff | annotate
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs; file | diff | annotate
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const; file | diff | annotate
Wed, 04 Jan 2012 12:09:53 +0100 blanchet improved "set" support by code inspection file | diff | annotate
Wed, 04 Jan 2012 12:09:53 +0100 blanchet tuning file | diff | annotate
Tue, 03 Jan 2012 23:41:59 +0100 blanchet fixed bisimilarity axiom -- avoid "insert" with wrong type file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet more robust destruction of "set Collect" idiom file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet handle starred predicates correctly w.r.t. "set" file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet simplify mem Collect file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet fixed set extensionality code file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet construct correct "set" type for wf goal file | diff | annotate
Tue, 03 Jan 2012 18:33:18 +0100 blanchet fixed Nitpick's typedef handling w.r.t. "set" file | diff | annotate
less more (0) -100 -60 tip
isabelle