src/HOL/Analysis/Sparse_In.thy
changeset 82913 7c870287f04f
parent 82518 da14e77a48b2