src/HOL/Lattices.thy
Thu, 05 Mar 2009 08:23:09 +0100 haftmann moved complete_lattice to Set.thy
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation
Thu, 11 Dec 2008 18:30:26 +0100 ballarin Conversion of HOL-Main and ZF to new locales.
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Mon, 27 Oct 2008 16:15:47 +0100 haftmann sup_bot and inf_top
Fri, 24 Oct 2008 17:48:37 +0200 haftmann new classes "top" and "bot"
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Fri, 25 Jul 2008 12:03:34 +0200 haftmann added class preorder
Wed, 07 May 2008 10:56:36 +0200 berghofe - Now imports Fun rather than Orderings
Fri, 07 Mar 2008 13:53:02 +0100 haftmann tuned proofs
Wed, 30 Jan 2008 10:57:46 +0100 haftmann dual orders and dual lattices
Fri, 30 Nov 2007 20:13:03 +0100 haftmann adjustions to due to instance target
Wed, 28 Nov 2007 09:01:37 +0100 haftmann dropped implicit assumption proof
Sat, 10 Nov 2007 23:03:52 +0100 wenzelm tuned specifications of 'notation';
Fri, 26 Oct 2007 21:22:17 +0200 haftmann localized monotonicity; tuned syntax
Fri, 19 Oct 2007 19:45:29 +0200 haftmann antisymmetry not a default intro rule any longer
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax
Sat, 29 Sep 2007 08:58:54 +0200 haftmann further localization
Tue, 18 Sep 2007 18:52:17 +0200 ballarin Simplified proofs due to transitivity reasoner setup.
Sat, 01 Sep 2007 18:17:36 +0200 wenzelm mono_Int/Un: proper proof, avoid illegal schematic type vars;
Mon, 20 Aug 2007 18:07:29 +0200 haftmann Sup now explicit parameter of complete_lattice
Tue, 07 Aug 2007 09:38:47 +0200 haftmann tuned
Tue, 24 Jul 2007 15:20:45 +0200 haftmann using class target
Fri, 20 Jul 2007 14:27:56 +0200 haftmann simplified HOL bootstrap
Thu, 14 Jun 2007 18:33:31 +0200 wenzelm tuned proofs: avoid implicit prems;
Thu, 24 May 2007 08:37:39 +0200 haftmann rudimentary class target implementation
Sat, 19 May 2007 11:33:22 +0200 haftmann no special treatment in naming of locale predicates stemming form classes
Thu, 10 May 2007 10:21:44 +0200 haftmann tuned
Fri, 20 Apr 2007 11:21:35 +0200 haftmann tuned
Thu, 29 Mar 2007 14:21:45 +0200 haftmann dropped legacy ML bindings
Fri, 16 Mar 2007 21:32:10 +0100 haftmann integrated with LOrder.thy
Fri, 09 Mar 2007 08:45:50 +0100 haftmann stepping towards uniform lattice theory development in HOL
Fri, 02 Mar 2007 15:43:15 +0100 haftmann prefix of class interpretation not mandatory any longer
Mon, 22 Jan 2007 19:00:29 +0100 nipkow simplified proofs
Sat, 20 Jan 2007 14:09:27 +0100 wenzelm tuned ML setup;
Tue, 16 Jan 2007 08:06:57 +0100 haftmann renamed locale partial_order to order
Sun, 10 Dec 2006 13:14:43 +0100 nipkow renaming
Sun, 10 Dec 2006 07:12:26 +0100 nipkow Modified lattice locale
Fri, 01 Dec 2006 17:22:28 +0100 haftmann stripped some legacy bindings
Wed, 15 Nov 2006 17:05:40 +0100 haftmann reworking of min/max lemmas
Sun, 12 Nov 2006 19:22:10 +0100 nipkow started reorgnization of lattice theories
Wed, 08 Nov 2006 19:48:34 +0100 haftmann renamed Lattice_Locales to Lattices
less more (0) tip