src/HOL/Complete_Lattices.thy
2013-03-10 haftmann 2013-03-10 generalized subclass relation; tuned proof
2013-03-05 hoelzl 2013-03-05 complete_linorder is also a complete_distrib_lattice
2013-02-20 hoelzl 2013-02-20 move auxiliary lemmas from Library/Extended_Reals to HOL image
2012-10-18 haftmann 2012-10-18 simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-02-26 haftmann 2012-02-26 retain syntax here
2012-02-26 haftmann 2012-02-26 tuned syntax declarations; tuned structure
2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
2012-02-23 haftmann 2012-02-23 moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann 2012-02-19 distributed lattice properties of predicates to places of instantiation
2012-01-07 haftmann 2012-01-07 use Inf/Sup_bool_def/apply as code equations
2011-12-29 haftmann 2011-12-29 fundamental theorems on Set.bind
2011-12-24 haftmann 2011-12-24 lattice type class instances for `set`; added code lemma for Set.bind
2011-09-20 haftmann 2011-09-20 official status for UN_singleton
2011-09-19 noschinl 2011-09-19 removed legacy lemmas in Complete_Lattices
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-13 huffman 2011-09-13 remove some redundant [simp] declarations; simplify some proofs;
2011-09-13 noschinl 2011-09-13 tune proofs
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-09-10 haftmann 2011-09-10 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.