#
a36dfb5f |
|
18-Jul-2019 |
paulson <lp15@cam.ac.uk> |
More results about measure and integration theory
|
#
551b6192 |
|
05-Mar-2019 |
haftmann <none@none> |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
#
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
241de186 |
|
22-Dec-2016 |
haftmann <none@none> |
proper logical constants
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
#
78a9e4a8 |
|
16-Sep-2016 |
hoelzl <none@none> |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel --HG-- extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222
|
#
9e5f909f |
|
05-Aug-2016 |
hoelzl <none@none> |
move measure theory from HOL-Probability to HOL-Multivariate_Analysis --HG-- rename : src/HOL/Probability/Binary_Product_Measure.thy => src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy rename : src/HOL/Probability/Bochner_Integration.thy => src/HOL/Multivariate_Analysis/Bochner_Integration.thy rename : src/HOL/Probability/Borel_Space.thy => src/HOL/Multivariate_Analysis/Borel_Space.thy rename : src/HOL/Probability/Caratheodory.thy => src/HOL/Multivariate_Analysis/Caratheodory.thy rename : src/HOL/Probability/Complete_Measure.thy => src/HOL/Multivariate_Analysis/Complete_Measure.thy rename : src/HOL/Probability/Embed_Measure.thy => src/HOL/Multivariate_Analysis/Embed_Measure.thy rename : src/HOL/Probability/Finite_Product_Measure.thy => src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy rename : src/HOL/Probability/Interval_Integral.thy => src/HOL/Multivariate_Analysis/Interval_Integral.thy rename : src/HOL/Probability/Lebesgue_Integral_Substitution.thy => src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy rename : src/HOL/Probability/Lebesgue_Measure.thy => src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy rename : src/HOL/Probability/Measurable.thy => src/HOL/Multivariate_Analysis/Measurable.thy rename : src/HOL/Probability/Measure_Space.thy => src/HOL/Multivariate_Analysis/Measure_Space.thy rename : src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy => src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy rename : src/HOL/Probability/Radon_Nikodym.thy => src/HOL/Multivariate_Analysis/Radon_Nikodym.thy rename : src/HOL/Probability/Regularity.thy => src/HOL/Multivariate_Analysis/Regularity.thy rename : src/HOL/Probability/Set_Integral.thy => src/HOL/Multivariate_Analysis/Set_Integral.thy rename : src/HOL/Probability/Sigma_Algebra.thy => src/HOL/Multivariate_Analysis/Sigma_Algebra.thy rename : src/HOL/Probability/measurable.ML => src/HOL/Multivariate_Analysis/measurable.ML extra : rebase_source : 30ab39c42165c1c5622833cf256065cbfff030f9
|
#
ee163328 |
|
29-Jul-2016 |
wenzelm <none@none> |
more accurate cong del; tuned proofs;
|
#
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
#
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
#
188a9299 |
|
16-Jun-2016 |
hoelzl <none@none> |
Probability: show that measures form a complete lattice --HG-- extra : rebase_source : bb357b4daf07004fdbda6bdf8f08655e7e37c742
|
#
82807e87 |
|
16-Jun-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
378858ac |
|
07-Jun-2016 |
Andreas Lochbihler <none@none> |
add theory of discrete subprobability distributions
|