src/HOL/Analysis/Sparse_In.thy
changeset 80528 6dec6b1f31f5
parent 79857 819c28a7280f
child 80768 c7723cc15de8
equal deleted inserted replaced
80523:532156e8f15f 80528:6dec6b1f31f5