summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | immler |

Thu, 15 Nov 2012 17:36:08 +0100 | |

changeset 50091 | b3b5dc2350b7 |

parent 50090 | 01203193dfa0 |

child 50092 | 39898c719339 |

corrected headers

src/HOL/Probability/Fin_Map.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Probability/Projective_Limit.thy | file | annotate | diff | comparison | revisions |

--- 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

--- 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 *)