src/HOL/Complete_Lattice.thy
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"
2010-03-06 huffman 2010-03-06 add some lemmas about complete lattices
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-10-06 haftmann 2009-10-06 added syntactic Inf and Sup
2009-09-24 haftmann 2009-09-24 added dual for complete lattice
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-09-18 haftmann 2009-09-18 INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-16 haftmann 2009-09-16 Inter and Union are mere abbreviations for Inf and Sup
2009-08-28 nipkow 2009-08-28 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory