src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 62825 e6e80a8bf624
parent 61975 b4b11391c676
equal deleted inserted replaced
62824:3498c66b5e55 62825:e6e80a8bf624