src/HOL/Complete_Lattice.thy
Fri, 09 Sep 2011 00:22:18 +0200 krauss added syntactic classes for "inf" and "sup"
Fri, 19 Aug 2011 19:33:31 +0200 haftmann more concise definition for Inf, Sup on bool
Tue, 09 Aug 2011 08:07:22 +0200 haftmann tuned header
Tue, 09 Aug 2011 08:06:15 +0200 haftmann more uniform naming scheme for Inf/INF and Sup/SUP lemmas
Mon, 08 Aug 2011 22:33:36 +0200 haftmann move legacy candiates to bottom; marked candidates for default simp rules
Mon, 08 Aug 2011 22:11:00 +0200 haftmann merged
Mon, 08 Aug 2011 19:30:18 +0200 haftmann dropped lemmas (Inf|Sup)_(singleton|binary)
Mon, 08 Aug 2011 19:21:11 +0200 haftmann dropped lemmas (Inf|Sup)_(singleton|binary)
Mon, 08 Aug 2011 11:47:41 -0700 huffman add lemmas INF_image, SUP_image
Mon, 08 Aug 2011 11:25:18 -0700 huffman declare {INF,SUP}_empty [simp]
Fri, 05 Aug 2011 23:06:54 +0200 haftmann tuned order: pushing INF and SUP to Inf and Sup
Fri, 05 Aug 2011 22:58:17 +0200 haftmann tuned order: pushing INF and SUP to Inf and Sup
Fri, 05 Aug 2011 22:45:57 +0200 haftmann generalized lemmas to complete lattices
Thu, 04 Aug 2011 19:29:52 +0200 haftmann solving duality problem for complete_distrib_lattice; tuned
Thu, 04 Aug 2011 07:33:08 +0200 haftmann tuned orthography
Thu, 04 Aug 2011 07:31:59 +0200 haftmann avoid yet unknown fact antiquotation
Wed, 03 Aug 2011 23:21:52 +0200 haftmann class complete_distrib_lattice
Sun, 24 Jul 2011 21:27:25 +0200 haftmann more coherent structure in and across theories
Fri, 22 Jul 2011 07:33:29 +0200 haftmann dropped errorneous hint
Thu, 21 Jul 2011 22:47:13 +0200 haftmann moved some lemmas
Wed, 20 Jul 2011 22:14:39 +0200 haftmann class complete_linorder
Mon, 18 Jul 2011 21:52:34 +0200 haftmann proof tuning
Mon, 18 Jul 2011 21:49:39 +0200 haftmann generalization; various notation and proof tuning
Mon, 18 Jul 2011 21:34:01 +0200 haftmann avoid misunderstandable names
Mon, 18 Jul 2011 21:15:51 +0200 haftmann moved lemmas to appropriate theory
Sun, 17 Jul 2011 22:24:08 +0200 haftmann more on complement
Sun, 17 Jul 2011 20:57:56 +0200 haftmann more consistent theorem names
Sun, 17 Jul 2011 20:46:51 +0200 haftmann more lemmas about SUP
Sun, 17 Jul 2011 20:29:54 +0200 haftmann structuring duals together
Sun, 17 Jul 2011 20:23:33 +0200 haftmann more lemmas about Sup
Sun, 17 Jul 2011 19:55:17 +0200 haftmann generalized INT_anti_mono
Sun, 17 Jul 2011 19:48:02 +0200 haftmann moving UNIV = ... equations to their proper theories
Sun, 17 Jul 2011 15:15:58 +0200 haftmann further generalization from sets to complete lattices
Sat, 16 Jul 2011 22:28:35 +0200 haftmann generalized some lemmas
Sat, 16 Jul 2011 22:04:02 +0200 haftmann consolidated bot and top classes, tuned notation
Sat, 16 Jul 2011 21:53:50 +0200 haftmann tuned notation
Thu, 14 Jul 2011 17:14:54 +0200 haftmann tuned notation and proofs
Thu, 14 Jul 2011 00:20:43 +0200 haftmann tuned lemma positions and proofs
Thu, 14 Jul 2011 00:16:41 +0200 haftmann tuned notation
Wed, 13 Jul 2011 19:43:12 +0200 haftmann moved lemmas bot_less and less_top to classes bot and top respectively
Wed, 13 Jul 2011 07:26:31 +0200 haftmann more generalization towards complete lattices
Sun, 10 Jul 2011 22:42:53 +0200 haftmann tuned proofs
Sun, 10 Jul 2011 22:17:33 +0200 haftmann tuned notation
Sun, 10 Jul 2011 22:11:32 +0200 haftmann tuned notation
Sun, 10 Jul 2011 21:56:39 +0200 haftmann tuned notation
Sun, 10 Jul 2011 15:45:35 +0200 haftmann tuned proofs and notation
Sun, 10 Jul 2011 14:26:07 +0200 haftmann more succinct proofs
Sun, 10 Jul 2011 14:14:19 +0200 haftmann more succinct proofs
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"
less more (0) -60 tip