src/HOL/Analysis/L2_Norm.thy
changeset 65865 177b90f33f40
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6