HOL-ex.Gauge_Integration