src/HOL/Integration.thy
changeset 33020 0908ed080ccf
parent 32960 69916a850301
child 33640 0d82107dc07a