| 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
|
| 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
|
| 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
|
| Thu, 05 Dec 2013 13:22:00 +0100 |
blanchet |
make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
|
file |
diff |
annotate
|
| Tue, 28 May 2013 18:12:21 +0200 |
blanchet |
tuned Nitpick message to be in sync with similar warning from Kodkod
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:00:24 +0200 |
blanchet |
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 11:28:56 +0100 |
blanchet |
more robust set element extractor
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
handle "Id" gracefully w.r.t. "set"
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
rationalized output (a bit)
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
fixed a few more bugs in \Nitpick's new "set" support
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
port part of Nitpick to "set" type constructor
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 16:49:21 +0200 |
blanchet |
worked around Kodkodi limitation with parsing {}, where it cannot easily deduce its arity -- without this workaround, Kodkod sometimes generates arity errors in conjunction with the "need" option since change 614ff13dc5d2
|
file |
diff |
annotate
|
| Sat, 19 Mar 2011 14:03:13 +0100 |
blanchet |
preencode value of "need" selectors in Kodkod bounds as an optimization
|
file |
diff |
annotate
|
| Sat, 19 Mar 2011 11:22:23 +0100 |
blanchet |
ignore "need" axioms for "nat"-like types
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 17:27:28 +0100 |
blanchet |
optimize Kodkod axioms further w.r.t. "need" option
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 12:20:32 +0100 |
blanchet |
optimize Kodkod bounds of nat-like datatypes
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 12:05:23 +0100 |
blanchet |
more optimizations of bounds for "need"
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 11:43:28 +0100 |
blanchet |
optimize Kodkod bounds when "need" is specified
|
file |
diff |
annotate
|
| Tue, 15 Mar 2011 15:49:42 +0100 |
blanchet |
support non-ground "need" values
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
renamed "preconstr" option "need"
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 17:36:32 +0100 |
blanchet |
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 16:33:21 +0100 |
blanchet |
more work on "fix_datatype_vals"
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 15:45:44 +0100 |
blanchet |
first steps in implementing "fix_datatype_vals" optimization
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:01 +0100 |
blanchet |
removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:01 +0100 |
blanchet |
simplified special handling of set products
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:01 +0100 |
blanchet |
use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
|
file |
diff |
annotate
|