src/HOL/Probability/Fin_Map.thy

-(*  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
   @{const Pi\<^isub>M}. *}