| changeset 41959 | b460124855b8 | 
| parent 41705 | 1100512e16d8 | 
| child 41981 | cdf7693bbe08 | 
| 41958:5abc60a017e0 | 41959:b460124855b8 | 
|---|---|
| 1 (* Title: Complete_Measure.thy | 1 (* Title: HOL/Probability/Complete_Measure.thy | 
| 2 Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen | 2 Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen | 
| 3 *) | 3 *) | 
| 4 | |
| 4 theory Complete_Measure | 5 theory Complete_Measure | 
| 5 imports Product_Measure | 6 imports Product_Measure | 
| 6 begin | 7 begin | 
| 7 | 8 | 
| 8 locale completeable_measure_space = measure_space | 9 locale completeable_measure_space = measure_space |