src/HOL/Analysis/Starlike.thy
changeset 78698 1b9388e6eb75
parent 78670 f8595f6d39a5
child 79566 f783490c6c99