summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Complete_Measure.thy

changeset 42146 | 5b52c6a9c627 |

parent 41983 | 2dc6e382a58b |

child 42866 | b0746bd57a41 |

1.1 --- a/src/HOL/Probability/Complete_Measure.thy Tue Mar 29 14:27:31 2011 +0200 1.2 +++ b/src/HOL/Probability/Complete_Measure.thy Tue Mar 29 14:27:39 2011 +0200 1.3 @@ -3,7 +3,7 @@ 1.4 *) 1.5 1.6 theory Complete_Measure 1.7 -imports Product_Measure 1.8 +imports Lebesgue_Integration 1.9 begin 1.10 1.11 locale completeable_measure_space = measure_space