src/HOL/Analysis/L2_Norm.thy
changeset 68000 40b790c5a11d
parent 67685 bdff8bf0a75b
child 68465 e699ca8e22b7