src/HOL/Complete_Lattice.thy
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Mon, 14 Mar 2011 14:37:36 +0100 hoelzl add lemmas for SUP and INF
Wed, 08 Dec 2010 15:05:46 +0100 haftmann bot comes before top, inf before sup etc.
Wed, 08 Dec 2010 14:52:23 +0100 haftmann nice syntax for lattice INFI, SUPR;
Thu, 02 Dec 2010 14:34:58 +0100 hoelzl Move SUP_commute, SUP_less_iff to HOL image;
Fri, 26 Nov 2010 16:28:34 +0100 wenzelm prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 24 Aug 2010 14:41:37 +0200 hoelzl moved generic lemmas in Probability to HOL
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Mon, 26 Apr 2010 09:37:46 -0700 huffman fix syntax precedence declarations for UNION, INTER, SUP, INF
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Sat, 06 Mar 2010 08:08:30 -0800 huffman add some lemmas about complete lattices
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Sat, 05 Dec 2009 20:02:21 +0100 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices
Tue, 06 Oct 2009 15:51:34 +0200 haftmann added syntactic Inf and Sup
Thu, 24 Sep 2009 18:29:28 +0200 haftmann added dual for complete lattice
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
Fri, 18 Sep 2009 14:09:38 +0200 haftmann INTER and UNION are mere abbreviations for INFI and SUPR
Wed, 16 Sep 2009 13:43:05 +0200 haftmann Inter and Union are mere abbreviations for Inf and Sup
Fri, 28 Aug 2009 18:52:41 +0200 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
Wed, 22 Jul 2009 18:02:10 +0200 haftmann moved complete_lattice &c. into separate theory
less more (0) tip