src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 59397 fc909f7e7ce5
parent 58877 262572d90bc6
child 59807 22bc39064290
equal deleted inserted replaced
59396:a2f4252c5489 59397:fc909f7e7ce5