History log of /seL4-l4v-master/isabelle/src/HOL/Probability/Conditional_Expectation.thy
Revision Date Author Comments
# a4784f6f 09-Oct-2019 haftmann <none@none>

dedicated fact collections for algebraic simplification rules potentially splitting goals

--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
# ce7a87d1 11-Apr-2019 paulson <lp15@cam.ac.uk>

type instantiations for poly_mapping as a real_normed_vector
# ab32308e 21-Jan-2019 paulson <lp15@cam.ac.uk>

renamings and new material
# b15d33eb 13-Apr-2018 paulson <lp15@cam.ac.uk>

Probability builds with new definitions
# 1387b04b 19-Dec-2017 wenzelm <none@none>

isabelle update_cartouches -c -t;
# a1e8064f 13-Oct-2016 hoelzl <none@none>

HOL-Probability: move conditional expectation from AFP/Ergodic_Theory

--HG--
extra : rebase_source : 55f4bbfc342a2532835d5bd35b92dd5cf39bc512