src/HOL/Analysis/Starlike.thy
changeset 78694 5e995ceb7490
parent 78670 f8595f6d39a5
child 79566 f783490c6c99