src/HOL/Analysis/Starlike.thy
changeset 76518 b30b8e23383c
parent 74729 64b3d8d9bd10
child 78037 37894dff0111