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