src/HOL/Analysis/Sparse_In.thy
changeset 82470 785615e37846
parent 82137 7281e57085ab
child 82518 da14e77a48b2