src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 55709 4e5a83a46ded
parent 54263 c4159fe6fa46
child 56223 7696903b9e61