src/HOL/Lattices_Big.thy
Thu, 11 Mar 2021 07:05:38 +0000 haftmann avoid name clash
Sun, 28 Feb 2021 20:13:07 +0000 haftmann dissolve theory with duplicated name from afp
Tue, 23 Feb 2021 20:41:48 +0000 haftmann dropped obscure FIXME
Mon, 08 Feb 2021 19:48:45 +0100 nipkow added lemmas
Fri, 08 Jan 2021 15:13:23 +0100 wenzelm isabelle update_cartouches;
Tue, 06 Oct 2020 16:55:56 +0200 nipkow added lemmas; internalized defn in class
Thu, 18 Apr 2019 16:34:04 +0200 nipkow added lemma
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 10 Nov 2018 07:57:20 +0000 haftmann replaced some ancient ASCII syntax
Wed, 12 Sep 2018 18:44:31 +0200 nipkow added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
Fri, 24 Aug 2018 20:22:10 +0000 haftmann deprecation of ASCII syntax for indexed big operators
Thu, 23 Aug 2018 17:09:39 +0000 haftmann simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
Thu, 23 Aug 2018 17:09:37 +0000 haftmann dropped redundant syntax translation rules for big operators
Thu, 23 Aug 2018 14:49:36 +0200 nipkow tuned lemmas
Wed, 22 Aug 2018 16:41:10 +0200 nipkow tuned lemmas
Wed, 22 Aug 2018 12:31:57 +0200 nipkow copied but not adapted
Mon, 09 Apr 2018 15:20:11 +0100 paulson Syntax for the special cases Min(A`I) and Max (A`I)
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Fri, 02 Feb 2018 11:47:13 +0100 nipkow added lemma
Sun, 28 Jan 2018 16:38:48 +0000 haftmann avoid concrete (anti)mono in theorem names since it could be the other way round
Wed, 13 Dec 2017 11:44:11 +0100 nipkow made arg_min_on definition
Wed, 08 Nov 2017 21:01:53 +0100 nipkow corrected priority
Tue, 15 Aug 2017 09:29:35 +0200 nipkow added Min_mset and Max_mset
Mon, 07 Aug 2017 11:21:11 +0200 blanchet tuning imports
Tue, 30 May 2017 14:04:48 +0200 nipkow tuned names
Tue, 30 May 2017 10:03:35 +0200 nipkow redefined Greatest
Sun, 28 May 2017 13:57:43 +0200 nipkow introduced arg_max
Sun, 28 May 2017 08:07:40 +0200 nipkow removed LeastM; is now arg_min
Sat, 27 May 2017 22:52:08 +0200 nipkow more arg_min
Tue, 16 May 2017 11:40:08 +0200 nipkow more arg_min
Sun, 14 May 2017 13:55:51 +0200 nipkow added function arg_min
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
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
Wed, 02 Dec 2015 19:14:57 +0100 haftmann modernized
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 28 Sep 2014 20:27:46 +0200 haftmann moved to HOL and generalized
Wed, 06 Aug 2014 18:03:43 +0200 nipkow added lemma
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
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Mon, 20 Jan 2014 23:34:26 +0100 blanchet swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Wed, 25 Dec 2013 17:39:07 +0100 haftmann abolished slightly odd global lattice interpretation for min/max
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Tue, 24 Dec 2013 11:24:16 +0100 haftmann tuning and augmentation of min/max lemmas;
Sun, 15 Dec 2013 15:10:16 +0100 haftmann disambiguation of interpretation prefixes
Sun, 15 Dec 2013 15:10:14 +0100 haftmann more algebraic terminology for theories about big operators
less more (0) tip