src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 56131 836b47c6531d
parent 54263 c4159fe6fa46
child 56223 7696903b9e61