| Wed, 07 Sep 2016 11:59:09 +0200 |
haftmann |
discontinued theory-local special syntax for lattice orderings
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 18:57:20 +0200 |
haftmann |
formal passive interpretation proofs for conj and disj
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 17:03:50 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:21:56 +0100 |
Andreas Lochbihler |
cancel complementary terms as arguments to sup/inf in boolean algebras
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
explicit equivalence for strict order on lattices
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
explicit distributivity facts on min/max
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
postponed min/max lemmas until abstract lattice is available
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
prefer abstract simp rule
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 10:09:43 +0100 |
haftmann |
more lemmas on abstract lattices
|
file |
diff |
annotate
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
examples for interpretation into target
|
file |
diff |
annotate
|
| Mon, 01 Apr 2013 17:42:29 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 21:53:56 +0100 |
haftmann |
more uniform style for interpretation and sublocale declarations
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:49:57 +0100 |
haftmann |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| Sun, 10 Mar 2013 14:36:03 +0100 |
nipkow |
stepwise instantiation is more modular
|
file |
diff |
annotate
|
| Sat, 22 Dec 2012 00:04:50 +0100 |
nipkow |
added simp rule
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:52:24 +0200 |
haftmann |
more explicit code equations
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 20:10:14 +0100 |
haftmann |
tuned syntax declarations; tuned structure
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 15:28:48 +0100 |
haftmann |
marked candidates for rule declarations
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 20:33:35 +0100 |
haftmann |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
| Sun, 19 Feb 2012 15:30:35 +0100 |
haftmann |
distributed lattice properties of predicates to places of instantiation
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:22:01 +0200 |
noschinl |
tune proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 22:33:36 +0200 |
haftmann |
move legacy candiates to bottom; marked candidates for default simp rules
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:24:08 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 21:56:39 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 15:05:46 +0100 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 14:52:23 +0100 |
haftmann |
nice syntax for lattice INFI, SUPR;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| 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
|