Skip to content
Success

Changes

Summary

  1. New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
Changeset 70694:ae37b8fbf023 by paulson _lp15@cam.ac.uk_:
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
The file was addedsrc/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Limits.thy (diff)