src/HOL/Analysis/L2_Norm.thy
changeset 69242 c911716d29bb
parent 69164 74f1b0f10b2b
child 69546 27dae626822b