src/HOL/Lattices_Big.thy
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