src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 60369 f393a3fe884c
parent 58877 262572d90bc6
child 60420 884f54e01427
equal deleted inserted replaced
60368:d3f561aa2af6 60369:f393a3fe884c