src/HOL/Complete_Lattice.thy
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