| 2015-05-28 |
paulson |
2015-05-28 |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
file | diff | annotate |
| 2015-05-04 |
hoelzl |
2015-05-04 |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file | diff | annotate |
| 2014-11-02 |
wenzelm |
2014-11-02 |
modernized header uniformly as section;
|
file | diff | annotate |
| 2014-06-30 |
hoelzl |
2014-06-30 |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file | diff | annotate |
| 2014-06-09 |
nipkow |
2014-06-09 |
Sup/Inf on functions decoupled from complete_lattice.
|
file | diff | annotate |
| 2014-04-26 |
haftmann |
2014-04-26 |
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
|
file | diff | annotate |
| 2014-04-26 |
haftmann |
2014-04-26 |
subsumed by existing default simp rules for functions and booleans
|
file | diff | annotate |
| 2014-03-22 |
haftmann |
2014-03-22 |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
file | diff | annotate |
| 2014-03-19 |
haftmann |
2014-03-19 |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file | diff | annotate |
| 2014-03-18 |
haftmann |
2014-03-18 |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
file | diff | annotate |
| 2014-03-16 |
haftmann |
2014-03-16 |
normalising simp rules for compound operators
|
file | diff | annotate |
| 2014-03-13 |
haftmann |
2014-03-13 |
dropped redundant theorems
|
file | diff | annotate |
| 2014-03-13 |
haftmann |
2014-03-13 |
monotonicity in complete lattices
|
file | diff | annotate |
| 2014-03-09 |
haftmann |
2014-03-09 |
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
* * *
tuned
|
file | diff | annotate |
| 2013-11-12 |
hoelzl |
2013-11-12 |
add equalities for SUP and INF over constant functions
|
file | diff | annotate |
| 2013-11-05 |
hoelzl |
2013-11-05 |
add SUP and INF for conditionally complete lattices
|
file | diff | annotate |
| 2013-11-05 |
hoelzl |
2013-11-05 |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file | diff | annotate |
| 2013-10-18 |
blanchet |
2013-10-18 |
killed most "no_atp", to make Sledgehammer more complete
|
file | diff | annotate |
| 2013-09-03 |
wenzelm |
2013-09-03 |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file | diff | annotate |
| 2013-08-13 |
wenzelm |
2013-08-13 |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file | diff | annotate |
| 2013-07-25 |
haftmann |
2013-07-25 |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file | diff | annotate |
| 2013-05-25 |
haftmann |
2013-05-25 |
weaker precendence of syntax for big intersection and union on sets
|
file | diff | annotate |
| 2013-03-26 |
haftmann |
2013-03-26 |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file | diff | annotate |
| 2013-03-23 |
haftmann |
2013-03-23 |
fundamental revision of big operators on sets
|
file | diff | annotate |
| 2013-03-10 |
haftmann |
2013-03-10 |
generalized subclass relation;
tuned proof
|
file | diff | annotate |
| 2013-03-05 |
hoelzl |
2013-03-05 |
complete_linorder is also a complete_distrib_lattice
|
file | diff | annotate |
| 2013-02-20 |
hoelzl |
2013-02-20 |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file | diff | annotate |
| 2012-10-18 |
haftmann |
2012-10-18 |
simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs
|
file | diff | annotate |
| 2012-03-12 |
noschinl |
2012-03-12 |
tuned proofs
|
file | diff | annotate |
| 2012-03-12 |
noschinl |
2012-03-12 |
tuned simpset
|
file | diff | annotate |
| 2012-02-26 |
haftmann |
2012-02-26 |
retain syntax here
|
file | diff | annotate |
| 2012-02-26 |
haftmann |
2012-02-26 |
tuned syntax declarations; tuned structure
|
file | diff | annotate |
| 2012-02-26 |
haftmann |
2012-02-26 |
marked candidates for rule declarations
|
file | diff | annotate |
| 2012-02-23 |
haftmann |
2012-02-23 |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
file | diff | annotate |
| 2012-02-21 |
haftmann |
2012-02-21 |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file | diff | annotate |
| 2012-02-19 |
haftmann |
2012-02-19 |
distributed lattice properties of predicates to places of instantiation
|
file | diff | annotate |
| 2012-01-07 |
haftmann |
2012-01-07 |
use Inf/Sup_bool_def/apply as code equations
|
file | diff | annotate |
| 2011-12-29 |
haftmann |
2011-12-29 |
fundamental theorems on Set.bind
|
file | diff | annotate |
| 2011-12-24 |
haftmann |
2011-12-24 |
lattice type class instances for `set`; added code lemma for Set.bind
|
file | diff | annotate |
| 2011-09-20 |
haftmann |
2011-09-20 |
official status for UN_singleton
|
file | diff | annotate |
| 2011-09-19 |
noschinl |
2011-09-19 |
removed legacy lemmas in Complete_Lattices
|
file | diff | annotate |
| 2011-09-15 |
hoelzl |
2011-09-15 |
removed further legacy rules from Complete_Lattices
|
file | diff | annotate |
| 2011-09-14 |
hoelzl |
2011-09-14 |
renamed Complete_Lattices lemmas, removed legacy names
|
file | diff | annotate |
| 2011-09-13 |
huffman |
2011-09-13 |
tuned proofs
|
file | diff | annotate |
| 2011-09-13 |
huffman |
2011-09-13 |
remove some redundant [simp] declarations;
simplify some proofs;
|
file | diff | annotate |
| 2011-09-13 |
noschinl |
2011-09-13 |
tune proofs
|
file | diff | annotate |
| 2011-09-13 |
noschinl |
2011-09-13 |
tune simpset for Complete_Lattices
|
file | diff | annotate |
| 2011-09-10 |
haftmann |
2011-09-10 |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file | diff | annotate | base |