src/HOL/Analysis/Sparse_In.thy
changeset 80642 318b1b75a4b8
parent 79857 819c28a7280f
child 80768 c7723cc15de8