Fri, 19 Oct 2007 19:45:29 +0200 |
haftmann |
antisymmetry not a default intro rule any longer
|
file |
diff |
annotate
|
Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
Sat, 29 Sep 2007 08:58:54 +0200 |
haftmann |
further localization
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 18:52:17 +0200 |
ballarin |
Simplified proofs due to transitivity reasoner setup.
|
file |
diff |
annotate
|
Sat, 01 Sep 2007 18:17:36 +0200 |
wenzelm |
mono_Int/Un: proper proof, avoid illegal schematic type vars;
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 18:07:29 +0200 |
haftmann |
Sup now explicit parameter of complete_lattice
|
file |
diff |
annotate
|
Tue, 07 Aug 2007 09:38:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Thu, 24 May 2007 08:37:39 +0200 |
haftmann |
rudimentary class target implementation
|
file |
diff |
annotate
|
Sat, 19 May 2007 11:33:22 +0200 |
haftmann |
no special treatment in naming of locale predicates stemming form classes
|
file |
diff |
annotate
|
Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Fri, 20 Apr 2007 11:21:35 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:10 +0100 |
haftmann |
integrated with LOrder.thy
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:15 +0100 |
haftmann |
prefix of class interpretation not mandatory any longer
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 19:00:29 +0100 |
nipkow |
simplified proofs
|
file |
diff |
annotate
|
Sat, 20 Jan 2007 14:09:27 +0100 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
Tue, 16 Jan 2007 08:06:57 +0100 |
haftmann |
renamed locale partial_order to order
|
file |
diff |
annotate
|
Sun, 10 Dec 2006 13:14:43 +0100 |
nipkow |
renaming
|
file |
diff |
annotate
|
Sun, 10 Dec 2006 07:12:26 +0100 |
nipkow |
Modified lattice locale
|
file |
diff |
annotate
|
Fri, 01 Dec 2006 17:22:28 +0100 |
haftmann |
stripped some legacy bindings
|
file |
diff |
annotate
|
Wed, 15 Nov 2006 17:05:40 +0100 |
haftmann |
reworking of min/max lemmas
|
file |
diff |
annotate
|
Sun, 12 Nov 2006 19:22:10 +0100 |
nipkow |
started reorgnization of lattice theories
|
file |
diff |
annotate
|
Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
file |
diff |
annotate
|