| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Wed, 05 May 2010 09:24:41 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:14:14 +0200 |
Cezary Kaliszyk |
add bounded_lattice_bot and bounded_lattice_top type classes
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 19:17:10 +0200 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 01:27:06 +0100 |
ballarin |
Tuned interpretation proofs.
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 12:49:14 -0700 |
huffman |
add/change some lemmas about lattices
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:38:20 +0100 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
distributed theory Algebras to theories Groups and Lattices
|
file |
diff |
annotate
|
| Fri, 12 Feb 2010 14:28:01 +0100 |
haftmann |
tuned import order
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:43 +0100 |
haftmann |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 20:02:21 +0100 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 17:16:01 +0200 |
haftmann |
moved lemmas about sup on bool to Lattices.thy
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 17:09:06 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 14 Sep 2009 08:36:57 +0200 |
haftmann |
some lemmas about strict order in lattices
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 15:39:02 +0200 |
haftmann |
proper class syntax for sublocale class < expr
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 18:52:41 +0200 |
nipkow |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:54 +0200 |
haftmann |
localized interpretation of min/max-lattice
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 15:54:19 +0200 |
haftmann |
refinement of lattice classes
|
file |
diff |
annotate
|
| Mon, 13 Jul 2009 08:25:43 +0200 |
haftmann |
removed outdated comment
|
file |
diff |
annotate
|
| Sat, 11 Jul 2009 21:33:01 +0200 |
haftmann |
added boolean_algebra type class; tuned lattice duals
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:09 +0100 |
haftmann |
moved complete_lattice to Set.thy
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:15:47 +0100 |
haftmann |
sup_bot and inf_top
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:37 +0200 |
haftmann |
new classes "top" and "bot"
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:36 +0200 |
berghofe |
- Now imports Fun rather than Orderings
|
file |
diff |
annotate
|
| Fri, 07 Mar 2008 13:53:02 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 30 Jan 2008 10:57:46 +0100 |
haftmann |
dual orders and dual lattices
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:03 +0100 |
haftmann |
adjustions to due to instance target
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:37 +0100 |
haftmann |
dropped implicit assumption proof
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 23:03:52 +0100 |
wenzelm |
tuned specifications of 'notation';
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 21:22:17 +0200 |
haftmann |
localized monotonicity; tuned syntax
|
file |
diff |
annotate
|
| 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
|