| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 06:48:02 +0000 |
haftmann |
earlier availability of lifting
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
dissolve theory with duplicated name from afp
|
file |
diff |
annotate
|
| Tue, 23 Feb 2021 20:41:48 +0000 |
haftmann |
dropped obscure FIXME
|
file |
diff |
annotate
|
| Mon, 08 Feb 2021 19:48:45 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 15:13:23 +0100 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2020 16:55:56 +0200 |
nipkow |
added lemmas; internalized defn in class
|
file |
diff |
annotate
|
| Thu, 18 Apr 2019 16:34:04 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:20 +0000 |
haftmann |
replaced some ancient ASCII syntax
|
file |
diff |
annotate
|
| Wed, 12 Sep 2018 18:44:31 +0200 |
nipkow |
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
|
file |
diff |
annotate
|
| Fri, 24 Aug 2018 20:22:10 +0000 |
haftmann |
deprecation of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Thu, 23 Aug 2018 17:09:39 +0000 |
haftmann |
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
|
file |
diff |
annotate
|
| Thu, 23 Aug 2018 17:09:37 +0000 |
haftmann |
dropped redundant syntax translation rules for big operators
|
file |
diff |
annotate
|
| Thu, 23 Aug 2018 14:49:36 +0200 |
nipkow |
tuned lemmas
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 16:41:10 +0200 |
nipkow |
tuned lemmas
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:31:57 +0200 |
nipkow |
copied but not adapted
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 15:20:11 +0100 |
paulson |
Syntax for the special cases Min(A`I) and Max (A`I)
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 02 Feb 2018 11:47:13 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 16:38:48 +0000 |
haftmann |
avoid concrete (anti)mono in theorem names since it could be the other way round
|
file |
diff |
annotate
|
| Wed, 13 Dec 2017 11:44:11 +0100 |
nipkow |
made arg_min_on definition
|
file |
diff |
annotate
|
| Wed, 08 Nov 2017 21:01:53 +0100 |
nipkow |
corrected priority
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 09:29:35 +0200 |
nipkow |
added Min_mset and Max_mset
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:21:11 +0200 |
blanchet |
tuning imports
|
file |
diff |
annotate
|
| Tue, 30 May 2017 14:04:48 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Tue, 30 May 2017 10:03:35 +0200 |
nipkow |
redefined Greatest
|
file |
diff |
annotate
|
| Sun, 28 May 2017 13:57:43 +0200 |
nipkow |
introduced arg_max
|
file |
diff |
annotate
|
| Sun, 28 May 2017 08:07:40 +0200 |
nipkow |
removed LeastM; is now arg_min
|
file |
diff |
annotate
|