src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 56866 c4512e94e15c
parent 56319 3bc95e0fa651
child 57512 cc97b347b301
equal deleted inserted replaced
56865:168766e28f5e 56866:c4512e94e15c