| Fri, 23 Feb 2018 14:32:59 +0100 |
wenzelm |
tuned signature -- eliminated clones;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2017 11:38:33 +0100 |
haftmann |
clarified comment
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
removed trailing final stops in Nitpick messages
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 17:03:09 +0100 |
blanchet |
made Nitpick more robust
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:55 +0100 |
haftmann |
consolidated name
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 22:24:37 +0100 |
blanchet |
removed needless ML function
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 15:57:25 +0200 |
blanchet |
avoid unsound simplification of (C (s x)) when s is a selector but not C's
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| 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
|