src/HOL/Hyperreal/Integration.thy
changeset 20625 1bb9a04f8c22
parent 20563 44eda2314aab
child 20792 add17d26151b