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

     2.1 --- a/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 16:07:52 2012 +0100
     2.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 17:36:08 2012 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Probability/Projective_Family.thy
     2.5 +(*  Title:      HOL/Probability/Projective_Limit.thy
     2.6      Author:     Fabian Immler, TU München
     2.7  *)
     2.8