src/HOL/Analysis/L2_Norm.thy
changeset 68724 7fafadbf16c7
parent 68607 67bb59e49834
child 69164 74f1b0f10b2b