changeset 68188 | 2af1f142f855 |
parent 68073 | fad29d2a17a5 |
child 68403 | 223172b97d0b |
--- a/src/HOL/Analysis/Sigma_Algebra.thy Tue May 15 06:23:12 2018 +0200 +++ b/src/HOL/Analysis/Sigma_Algebra.thy Tue May 15 11:33:43 2018 +0200 @@ -11,6 +11,7 @@ imports Complex_Main "HOL-Library.Countable_Set" + "HOL-Library.FuncSet" "HOL-Library.Indicator_Function" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Disjoint_Sets"