src/HOL/Analysis/Starlike.thy
changeset 81445 82110cbcf9a1
parent 81142 6ad2c917dd2e