src/HOL/Analysis/L2_Norm.thy
changeset 67963 9541f2c5ce8d
parent 67685 bdff8bf0a75b
child 68465 e699ca8e22b7