src/HOL/Analysis/Starlike.thy
changeset 74270 ad2899cdd528
parent 74007 df976eefcba0
child 74729 64b3d8d9bd10