summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Fin_Map.thy

changeset 50091 | b3b5dc2350b7 |

parent 50088 | 32d1795cc77a |

child 50094 | 84ddcf5364b4 |

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