src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 56253 83b3c110f22d
parent 56223 7696903b9e61
child 56319 3bc95e0fa651