src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 63220 06cbfbaf39c5
parent 61975 b4b11391c676
equal deleted inserted replaced
63219:a5697f7a3322 63220:06cbfbaf39c5