src/HOL/Probability/Radon_Nikodym.thy
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