src/HOL/Hyperreal/Star.thy
changeset 16123 1381e90c2694
parent 15170 e7d4d3314f4c
child 17298 ad73fb6144cf