src/HOL/Lattices_Big.thy
22 months ago nipkow 2017-08-15 added Min_mset and Max_mset
22 months ago blanchet 2017-08-07 tuning imports
2017-05-30 nipkow 2017-05-30 tuned names
2017-05-30 nipkow 2017-05-30 redefined Greatest
2017-05-28 nipkow 2017-05-28 introduced arg_max
2017-05-28 nipkow 2017-05-28 removed LeastM; is now arg_min
2017-05-27 nipkow 2017-05-27 more arg_min
2017-05-16 nipkow 2017-05-16 more arg_min
2017-05-14 nipkow 2017-05-14 added function arg_min
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-06-11 haftmann 2016-06-11 boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2015-12-02 haftmann 2015-12-02 modernized
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-28 haftmann 2014-09-28 moved to HOL and generalized
2014-08-06 nipkow 2014-08-06 added lemma
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-03-14 wenzelm 2014-03-14 just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-01-20 blanchet 2014-01-20 swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-25 haftmann 2013-12-25 abolished slightly odd global lattice interpretation for min/max
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-24 haftmann 2013-12-24 tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs
2013-12-15 haftmann 2013-12-15 disambiguation of interpretation prefixes
2013-12-15 haftmann 2013-12-15 more algebraic terminology for theories about big operators