src/HOL/Complete_Lattice.thy
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-08-19 haftmann 2011-08-19 more concise definition for Inf, Sup on bool
2011-08-09 haftmann 2011-08-09 tuned header
2011-08-09 haftmann 2011-08-09 more uniform naming scheme for Inf/INF and Sup/SUP lemmas
2011-08-08 haftmann 2011-08-08 move legacy candiates to bottom; marked candidates for default simp rules
2011-08-08 haftmann 2011-08-08 merged
2011-08-08 haftmann 2011-08-08 dropped lemmas (Inf|Sup)_(singleton|binary)
2011-08-08 haftmann 2011-08-08 dropped lemmas (Inf|Sup)_(singleton|binary)
2011-08-08 huffman 2011-08-08 add lemmas INF_image, SUP_image
2011-08-08 huffman 2011-08-08 declare {INF,SUP}_empty [simp]
2011-08-05 haftmann 2011-08-05 tuned order: pushing INF and SUP to Inf and Sup
2011-08-05 haftmann 2011-08-05 tuned order: pushing INF and SUP to Inf and Sup
2011-08-05 haftmann 2011-08-05 generalized lemmas to complete lattices
2011-08-04 haftmann 2011-08-04 solving duality problem for complete_distrib_lattice; tuned
2011-08-04 haftmann 2011-08-04 tuned orthography
2011-08-04 haftmann 2011-08-04 avoid yet unknown fact antiquotation
2011-08-03 haftmann 2011-08-03 class complete_distrib_lattice
2011-07-24 haftmann 2011-07-24 more coherent structure in and across theories
2011-07-22 haftmann 2011-07-22 dropped errorneous hint
2011-07-21 haftmann 2011-07-21 moved some lemmas
2011-07-20 haftmann 2011-07-20 class complete_linorder
2011-07-18 haftmann 2011-07-18 proof tuning
2011-07-18 haftmann 2011-07-18 generalization; various notation and proof tuning
2011-07-18 haftmann 2011-07-18 avoid misunderstandable names
2011-07-18 haftmann 2011-07-18 moved lemmas to appropriate theory
2011-07-17 haftmann 2011-07-17 more on complement
2011-07-17 haftmann 2011-07-17 more consistent theorem names
2011-07-17 haftmann 2011-07-17 more lemmas about SUP
2011-07-17 haftmann 2011-07-17 structuring duals together
2011-07-17 haftmann 2011-07-17 more lemmas about Sup
2011-07-17 haftmann 2011-07-17 generalized INT_anti_mono
2011-07-17 haftmann 2011-07-17 moving UNIV = ... equations to their proper theories
2011-07-17 haftmann 2011-07-17 further generalization from sets to complete lattices
2011-07-16 haftmann 2011-07-16 generalized some lemmas
2011-07-16 haftmann 2011-07-16 consolidated bot and top classes, tuned notation
2011-07-16 haftmann 2011-07-16 tuned notation
2011-07-14 haftmann 2011-07-14 tuned notation and proofs
2011-07-14 haftmann 2011-07-14 tuned lemma positions and proofs
2011-07-14 haftmann 2011-07-14 tuned notation
2011-07-13 haftmann 2011-07-13 moved lemmas bot_less and less_top to classes bot and top respectively
2011-07-13 haftmann 2011-07-13 more generalization towards complete lattices
2011-07-10 haftmann 2011-07-10 tuned proofs
2011-07-10 haftmann 2011-07-10 tuned notation
2011-07-10 haftmann 2011-07-10 tuned notation
2011-07-10 haftmann 2011-07-10 tuned notation
2011-07-10 haftmann 2011-07-10 tuned proofs and notation
2011-07-10 haftmann 2011-07-10 more succinct proofs
2011-07-10 haftmann 2011-07-10 more succinct proofs
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-03-14 hoelzl 2011-03-14 add lemmas for SUP and INF
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-02 hoelzl 2010-12-02 Move SUP_commute, SUP_less_iff to HOL image; Cleanup generic complete_lattice lemmas in Positive_Infinite_Real; Cleanup lemma positive_integral_alt;
2010-11-26 wenzelm 2010-11-26 prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-08-24 hoelzl 2010-08-24 moved generic lemmas in Probability to HOL
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-26 huffman 2010-04-26 fix syntax precedence declarations for UNION, INTER, SUP, INF
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"