| Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add equalities for SUP and INF over constant functions
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:59 +0100 |
hoelzl |
add SUP and INF for conditionally complete lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:57 +0100 |
hoelzl |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
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
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
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
|
| Sun, 10 Mar 2013 11:21:16 +0100 |
haftmann |
generalized subclass relation;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 15:43:12 +0100 |
hoelzl |
complete_linorder is also a complete_distrib_lattice
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 09:19:37 +0200 |
haftmann |
simp results for simplification results of Inf/Sup expressions on bool;
|
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 21:25:54 +0100 |
haftmann |
retain syntax here
|
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
|
| Sat, 07 Jan 2012 20:18:56 +0100 |
haftmann |
use Inf/Sup_bool_def/apply as code equations
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 14:23:40 +0100 |
haftmann |
fundamental theorems on Set.bind
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:07 +0100 |
haftmann |
lattice type class instances for `set`; added code lemma for Set.bind
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 22:11:22 +0200 |
haftmann |
official status for UN_singleton
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 14:35:51 +0200 |
noschinl |
removed legacy lemmas in Complete_Lattices
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 08:21:51 -0700 |
huffman |
remove some redundant [simp] declarations;
|
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
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
| base
|