src/HOL/Hyperreal/ExtraThms2.ML
changeset 13413 0b60b9e18a26
parent 13153 4b052946b41c
child 13810 c3fbfd472365