--- a/src/HOL/Probability/Fin_Map.thy Thu Nov 15 16:07:52 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Thu Nov 15 17:36:08 2012 +0100
@@ -1,13 +1,13 @@
-(* Title: HOL/Probability/Projective_Family.thy
+(* Title: HOL/Probability/Fin_Map.thy
Author: Fabian Immler, TU München
*)
+header {* Finite Maps *}
+
theory Fin_Map
imports Finite_Product_Measure
begin
-section {* Finite Maps *}
-
text {* Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of
projective limit. @{const extensional} functions are used for the representation in order to
stay close to the developments of (finite) products @{const Pi\<^isub>E} and their sigma-algebra