| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| 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, 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
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
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
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
optimized MaSh output by chunking it
|
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
|
| Wed, 25 Apr 2012 14:33:21 +0200 |
blanchet |
improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things
|
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
|
| Wed, 04 Jan 2012 12:09:53 +0100 |
blanchet |
improved "set" support by code inspection
|
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
|
| Tue, 19 Apr 2011 11:56:11 +0200 |
blanchet |
check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 17:53:10 +0100 |
blanchet |
added "total_consts" option
|
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 |
fix special handling of set products
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:44:43 +0200 |
blanchet |
eliminate more clutter related to "fast_descrs" optimization
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:24:18 +0200 |
blanchet |
remove "fast_descs" option from Nitpick;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 20:15:04 +0200 |
blanchet |
move equation up where it's not ignored
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|