| #
551b6192 |
|
05-Mar-2019 |
haftmann <none@none> |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
| #
ec600d16 |
|
30-Dec-2018 |
haftmann <none@none> |
prefer naming convention from datatype package for strong congruence rules
|
| #
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
| #
ba9cb2ae |
|
18-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
1387b04b |
|
19-Dec-2017 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
f63c7c02 |
|
20-Oct-2016 |
hoelzl <none@none> |
HOL-Probability: move stopping time from AFP/Markov_Models
|
| #
c0dd9fff |
|
03-Oct-2016 |
hoelzl <none@none> |
Probability: move some theorems from AFP/Density_Compiler
|
| #
fad39d02 |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14
|
| #
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
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
188a9299 |
|
16-Jun-2016 |
hoelzl <none@none> |
Probability: show that measures form a complete lattice
--HG--
extra : rebase_source : bb357b4daf07004fdbda6bdf8f08655e7e37c742
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
79d3be54 |
|
14-Apr-2016 |
hoelzl <none@none> |
Probability: move emeasure and nn_integral from ereal to ennreal
--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77
|
| #
97ac1d28 |
|
01-Jan-2016 |
wenzelm <none@none> |
more symbols;
|
| #
ec168a56 |
|
17-Dec-2015 |
hoelzl <none@none> |
moved some theorems from the CLT proof; reordered some theorems / notation
--HG--
extra : rebase_source : 1d6aa5a56a9cef16ce4943372f5c681e16d0eb8b
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
81bb9693 |
|
28-Nov-2015 |
wenzelm <none@none> |
removed junk;
|
| #
ef370569 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
| #
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
| #
7fd06540 |
|
04-Nov-2015 |
ballarin <none@none> |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
23d5df30 |
|
07-Oct-2015 |
hoelzl <none@none> |
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
84c5ac0a |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
lemmas about integrals over bind and join on measures
|
| #
d6921607 |
|
08-Apr-2015 |
wenzelm <none@none> |
eliminated suspicious Unicode character;
|
| #
5c61fbef |
|
23-Mar-2015 |
hoelzl <none@none> |
add measurable_submarkov
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
a3a520af |
|
19-Feb-2015 |
haftmann <none@none> |
more canonical order of subscriptions avoids superfluous facts
--HG--
extra : rebase_source : 4626a7762a2840ce4891fcaa6d3121f5f8d7bd20
|
| #
44c356fa |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
more lemmas
|
| #
0ed8f303 |
|
22-Jan-2015 |
Andreas Lochbihler <none@none> |
generalise lemma
|
| #
6c7ab2bf |
|
22-Jan-2015 |
hoelzl <none@none> |
import general thms from Density_Compiler
--HG--
extra : rebase_source : 48a3b47f755d8099564008b93076eae81453a674
|
| #
2dd36018 |
|
04-Dec-2014 |
hoelzl <none@none> |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
--HG--
extra : rebase_source : 8c7131ba8a4f577186bc3393e7116b70e552dd7e
|
| #
ce7c103d |
|
23-Nov-2014 |
hoelzl <none@none> |
add congruence solver to measurability prover
--HG--
extra : rebase_source : 77341231f7d3ba19edd6c5865552541156a3dd71
|
| #
92a516b8 |
|
14-Nov-2014 |
hoelzl <none@none> |
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
262ef7f2 |
|
07-Oct-2014 |
hoelzl <none@none> |
fix document generation for HOL-Probability
|
| #
e46f9abe |
|
07-Oct-2014 |
hoelzl <none@none> |
add Giry monad
--HG--
extra : rebase_source : 3ceb1c0fa2e24cb05e37856566255a7b56f80af7
|