diff -r 01203193dfa0 -r b3b5dc2350b7 src/HOL/Probability/Fin_Map.thy
--- 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