| 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
|
| Sat, 27 May 2017 22:52:08 +0200 |
nipkow |
more arg_min
|
file |
diff |
annotate
|
| Tue, 16 May 2017 11:40:08 +0200 |
nipkow |
more arg_min
|
file |
diff |
annotate
|
| Sun, 14 May 2017 13:55:51 +0200 |
nipkow |
added function arg_min
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 20:33:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Wed, 02 Dec 2015 19:14:57 +0100 |
haftmann |
modernized
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2014 20:27:46 +0200 |
haftmann |
moved to HOL and generalized
|
file |
diff |
annotate
|
| Wed, 06 Aug 2014 18:03:43 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:34:26 +0100 |
blanchet |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:07 +0100 |
haftmann |
abolished slightly odd global lattice interpretation for min/max
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:16 +0100 |
haftmann |
disambiguation of interpretation prefixes
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
file |
diff |
annotate
|