src/HOL/Multivariate_Analysis/L2_Norm.thy
changeset 62101 26c0a70f78a3
parent 60974 6a6f15d8fbc4
equal deleted inserted replaced
62100:7a5754afe170 62101:26c0a70f78a3