src/HOL/Library/Product_Order.thy
19 months ago Manuel Eberl 2018-03-12 Changes to complete distributive lattices due to Viorel Preoteasa
23 months ago wenzelm 2017-11-26 more symbols;
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-04 wenzelm 2016-01-04 tuned proofs;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-03-19 haftmann 2014-03-19 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 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2013-12-16 immler 2013-12-16 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-02-14 haftmann 2013-02-14 consolidation of library theories on product orders