src/HOL/Analysis/Starlike.thy
changeset 68031 eda52f4cd4e4
parent 67990 c0ebecf6e3eb
child 68056 9e077a905209
child 68072 493b818e8e10