changeset 69517 | dc20f278e8f3 |
parent 69180 | 922833cc6839 |
child 69712 | dc85b5b3a532 |
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Thu Dec 27 23:38:55 2018 +0100 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Fri Dec 28 10:29:59 2018 +0100 @@ -6,7 +6,7 @@ This could probably be weakened somehow. *) -section \<open>Integration by Substition for the Lebesgue integral\<close> +section \<open>Integration by Substition for the Lebesgue Integral\<close> theory Lebesgue_Integral_Substitution imports Interval_Integral