src/HOL/Hyperreal/Integration.thy
changeset 23024 70435ffe077d
parent 22998 97e1f9c2cc46
child 23315 df3a7e9ebadb