src/HOL/Analysis/Sparse_In.thy
changeset 82967 73af47bc277c
parent 82518 da14e77a48b2
equal deleted inserted replaced
82966:55a71dd13ca0 82967:73af47bc277c