src/HOL/Analysis/L2_Norm.thy
changeset 68236 b4484ec4a8f7
parent 67685 bdff8bf0a75b
child 68465 e699ca8e22b7