src/HOL/Multivariate_Analysis/Operator_Norm.thy
changeset 50497 492953de3090
parent 44133 691c52e900ca
child 50526 899c9c4e4a4c
equal deleted inserted replaced
50496:8665ec681e47 50497:492953de3090