src/HOL/Analysis/Operator_Norm.thy
changeset 75513 36316c6a3fc2
parent 70136 f03a01a18c6e
equal deleted inserted replaced
75512:2251548ec4a8 75513:36316c6a3fc2