src/HOL/Analysis/L2_Norm.thy
changeset 63853 d0e8921da311
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75