src/HOL/Analysis/Starlike.thy
changeset 78778 d495e71707d4
parent 78670 f8595f6d39a5
child 79566 f783490c6c99