src/HOL/Hyperreal/Star.thy
changeset 16142 8eead5356ccb
parent 15170 e7d4d3314f4c
child 17298 ad73fb6144cf