changeset 42067 | 66c8281349ec |
parent 41981 | cdf7693bbe08 |
child 42866 | b0746bd57a41 |
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 18:53:05 2011 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 20:06:10 2011 +0100 @@ -1,3 +1,9 @@ +(* Title: HOL/Probability/Radon_Nikodym.thy + Author: Johannes Hölzl, TU München +*) + +header {*Radon-Nikod{\'y}m derivative*} + theory Radon_Nikodym imports Lebesgue_Integration begin