src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 56403 ae4f904c98b0
parent 56319 3bc95e0fa651
child 57512 cc97b347b301