src/HOL/Analysis/L2_Norm.thy
changeset 64454 4c868fa9d79b
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6