src/HOL/Analysis/L2_Norm.thy
changeset 68344 3bb44c25ce8b
parent 67685 bdff8bf0a75b
child 68465 e699ca8e22b7