| #
8b81086d |
|
09-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Syntax for the special cases Min(A`I) and Max (A`I)
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
70dfe670 |
|
02-Feb-2018 |
nipkow <none@none> |
added lemma
|
| #
3cc77c85 |
|
28-Jan-2018 |
haftmann <none@none> |
avoid concrete (anti)mono in theorem names since it could be the other way round
--HG--
extra : rebase_source : 99c2bd425eb6f44b37c6e989a08ec0fbefe25b2b
|
| #
5705225b |
|
13-Dec-2017 |
nipkow <none@none> |
made arg_min_on definition
|
| #
63d138f7 |
|
08-Nov-2017 |
nipkow <none@none> |
corrected priority
|
| #
7995a135 |
|
15-Aug-2017 |
nipkow <none@none> |
added Min_mset and Max_mset
|
| #
daac7840 |
|
07-Aug-2017 |
blanchet <none@none> |
tuning imports
|
| #
4281cde0 |
|
30-May-2017 |
nipkow <none@none> |
tuned names
|
| #
14753e1c |
|
30-May-2017 |
nipkow <none@none> |
redefined Greatest
|
| #
742e8eed |
|
28-May-2017 |
nipkow <none@none> |
introduced arg_max
|
| #
2a21fb9f |
|
28-May-2017 |
nipkow <none@none> |
removed LeastM; is now arg_min
|
| #
4b172f1d |
|
27-May-2017 |
nipkow <none@none> |
more arg_min
|
| #
3cb91b98 |
|
16-May-2017 |
nipkow <none@none> |
more arg_min
|
| #
b5ae810f |
|
14-May-2017 |
nipkow <none@none> |
added function arg_min
|
| #
6d0b05b4 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
0522687a |
|
11-Jun-2016 |
haftmann <none@none> |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
--HG--
extra : rebase_source : 4542f54b0b7fe6c0bea5be2116706e4cfacadaf0
|
| #
e089ca2f |
|
02-Dec-2015 |
haftmann <none@none> |
modernized
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
9254e49c |
|
28-Sep-2014 |
haftmann <none@none> |
moved to HOL and generalized
|
| #
f52cc5d5 |
|
06-Aug-2014 |
nipkow <none@none> |
added lemma
|
| #
1a8832ef |
|
18-May-2014 |
hoelzl <none@none> |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
--HG--
rename : src/HOL/Probability/Lebesgue_Integration.thy => src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
|
| #
7d65fe17 |
|
14-Mar-2014 |
wenzelm <none@none> |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
more thorough background_notes: distribute global notes to all contexts;
|
| #
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
| #
9f589a46 |
|
20-Jan-2014 |
blanchet <none@none> |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
| #
13c9f359 |
|
27-Dec-2013 |
haftmann <none@none> |
prefer target-style syntaxx for sublocale
|
| #
a3f109dd |
|
25-Dec-2013 |
haftmann <none@none> |
abolished slightly odd global lattice interpretation for min/max
|
| #
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
| #
f71fdda3 |
|
24-Dec-2013 |
haftmann <none@none> |
tuning and augmentation of min/max lemmas;
more lemmas and simp rules for abstract lattices with order;
tuned proofs
|
| #
31f5a7d3 |
|
15-Dec-2013 |
haftmann <none@none> |
disambiguation of interpretation prefixes
|
| #
2c9578d4 |
|
15-Dec-2013 |
haftmann <none@none> |
more algebraic terminology for theories about big operators
|