src/HOL/Analysis/L2_Norm.thy
changeset 65897 94b0da1b242e
parent 64267 b9a1486e79be
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
65896:18f5014331a1 65897:94b0da1b242e