src/HOL/Analysis/L2_Norm.thy
changeset 68004 a8a20be7053a
parent 67685 bdff8bf0a75b
child 68465 e699ca8e22b7