# HG changeset patch
# User immler
# Date 1352997368 3600
# Node ID b3b5dc2350b7b8c48eb5f4d8e7a3ff198efd5d17
# Parent 01203193dfa07c8f16ac8bc9ad005b9623adee17
corrected headers
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 sigmaalgebra
diff r 01203193dfa0 r b3b5dc2350b7 src/HOL/Probability/Projective_Limit.thy
 a/src/HOL/Probability/Projective_Limit.thy Thu Nov 15 16:07:52 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Thu Nov 15 17:36:08 2012 +0100
@@ 1,4 +1,4 @@
(* Title: HOL/Probability/Projective_Family.thy
+(* Title: HOL/Probability/Projective_Limit.thy
Author: Fabian Immler, TU München
*)