src/HOL/Library/Product_Order.thy
2019-03-10 wenzelm more formal contributors (with the help of the history);
2019-03-05 haftmann avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
2018-11-18 haftmann removed legacy input syntax
2018-11-08 haftmann removed relics of ASCII syntax for indexed big operators
2018-03-12 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
2017-11-26 wenzelm more symbols;
2016-09-30 hoelzl Library: fix name Product_plus to Product_Plus
2016-07-29 Andreas Lochbihler add lemmas contributed by Peter Gammie
2016-02-17 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-04 wenzelm tuned proofs;
2015-09-13 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-07-06 wenzelm tuned proofs;
2015-06-25 wenzelm tuned proofs;
2015-06-17 wenzelm isabelle update_cartouches;
2014-11-02 wenzelm modernized header;
2014-03-19 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann normalising simp rules for compound operators
2014-03-15 haftmann more complete set of lemmas wrt. image and composition
2013-12-16 immler ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-07-25 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-03-26 wenzelm tuned imports;
2013-02-14 haftmann consolidation of library theories on product orders
less more (0) tip