Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/Library/Product_Order.thy
2019-03-10
wenzelm
more formal contributors (with the help of the history);
file
|
diff
|
annotate
2019-03-05
haftmann
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
file
|
diff
|
annotate
2018-11-18
haftmann
removed legacy input syntax
file
|
diff
|
annotate
2018-11-08
haftmann
removed relics of ASCII syntax for indexed big operators
file
|
diff
|
annotate
2018-03-12
Manuel Eberl
Changes to complete distributive lattices due to Viorel Preoteasa
file
|
diff
|
annotate
2017-11-26
wenzelm
more symbols;
file
|
diff
|
annotate
2016-09-30
hoelzl
Library: fix name Product_plus to Product_Plus
file
|
diff
|
annotate
2016-07-29
Andreas Lochbihler
add lemmas contributed by Peter Gammie
file
|
diff
|
annotate
2016-02-17
haftmann
prefer abbreviations for compound operators INFIMUM and SUPREMUM
file
|
diff
|
annotate
2016-01-04
wenzelm
tuned proofs;
file
|
diff
|
annotate
2015-09-13
wenzelm
renamed method "goals" to "goal_cases" to emphasize its meaning;
file
|
diff
|
annotate
2015-07-06
wenzelm
tuned proofs;
file
|
diff
|
annotate
2015-06-25
wenzelm
tuned proofs;
file
|
diff
|
annotate
2015-06-17
wenzelm
isabelle update_cartouches;
file
|
diff
|
annotate
2014-11-02
wenzelm
modernized header;
file
|
diff
|
annotate
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
file
|
diff
|
annotate
2014-03-18
haftmann
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
file
|
diff
|
annotate
2014-03-16
haftmann
normalising simp rules for compound operators
file
|
diff
|
annotate
2014-03-15
haftmann
more complete set of lemmas wrt. image and composition
file
|
diff
|
annotate
2013-12-16
immler
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
file
|
diff
|
annotate
2013-07-25
haftmann
factored syntactic type classes for bot and top (by Alessandro Coglio)
file
|
diff
|
annotate
2013-03-26
wenzelm
tuned imports;
file
|
diff
|
annotate
2013-02-14
haftmann
consolidation of library theories on product orders
file
|
diff
|
annotate
|
base
less
more
(0)
tip