src/HOL/Analysis/Starlike.thy
changeset 75866 9eeed5c424f9
parent 74729 64b3d8d9bd10
child 78037 37894dff0111