src/HOL/Analysis/L2_Norm.thy
changeset 66230 ae814012b95f
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6