src/HOL/Analysis/Sparse_In.thy
changeset 80943 258b76a8b099
parent 80914 d97fdabd9e2b
child 81097 6c81cdca5b82
equal deleted inserted replaced
80942:501ebf1fc308 80943:258b76a8b099