src/HOL/Analysis/L2_Norm.thy
changeset 66378 53a6c5d4d03e
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6