| #
a1c1e852 |
|
14-Jun-2019 |
haftmann <none@none> |
official fact collection sign_simps
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
1d1ca5f1 |
|
08-Oct-2017 |
haftmann <none@none> |
avoid name clashes on interpretation of abstract locales
--HG--
extra : rebase_source : f524b077cafad9e920061f751ff3126d7a903434
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
| #
8f4f8db9 |
|
15-Apr-2016 |
hoelzl <none@none> |
fix HOL-Probability-ex
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
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.
|
| #
ae913163 |
|
30-Sep-2015 |
paulson <lp15@cam.ac.uk> |
real_of_nat_Suc is now a simprule
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
41682711 |
|
19-Jun-2015 |
nipkow <none@none> |
renamed multiset_of -> mset
|
| #
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
51c0565b |
|
09-Oct-2012 |
hoelzl <none@none> |
simplified definitions
|
| #
bf7737b4 |
|
09-Oct-2012 |
hoelzl <none@none> |
remove unnecessary assumption from conditional_entropy_eq
|
| #
11c87ed0 |
|
22-Apr-2012 |
hoelzl <none@none> |
reworked Probability theory
--HG--
extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41
|
| #
33cd0191 |
|
28-Feb-2012 |
wenzelm <none@none> |
avoid undeclared variables in let bindings;
tuned proofs;
|
| #
74f532bc |
|
01-Dec-2011 |
hoelzl <none@none> |
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
|
| #
d5c9d81f |
|
01-Dec-2011 |
hoelzl <none@none> |
moved theorems about distribution to the definition; removed oopsed-lemma
|
| #
4150e14d |
|
01-Dec-2011 |
hoelzl <none@none> |
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
7f546ab9 |
|
19-Jul-2011 |
hoelzl <none@none> |
Rename extreal => ereal
--HG--
rename : src/HOL/Library/Extended_Reals.thy => src/HOL/Library/Extended_Real.thy
|
| #
45c135d8 |
|
05-Apr-2011 |
hoelzl <none@none> |
Rename extensional to extensionalD (extensional is also defined in FuncSet)
|
| #
6c82f941 |
|
14-Mar-2011 |
hoelzl <none@none> |
reworked Probability theory: measures are not type restricted to positive extended reals
|
| #
93b9a16c |
|
01-Feb-2011 |
hoelzl <none@none> |
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv.
introduced binder variants for simple_integral, positive_integral and integral.
|
| #
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
| #
8dce21d4 |
|
03-Dec-2010 |
hoelzl <none@none> |
it is known as the extended reals, not the infinite reals
--HG--
rename : src/HOL/Probability/Positive_Infinite_Real.thy => src/HOL/Probability/Positive_Extended_Real.thy
|
| #
481ae947 |
|
01-Dec-2010 |
hoelzl <none@none> |
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
--HG--
rename : src/HOL/Probability/Borel.thy => src/HOL/Probability/Borel_Space.thy
|