src/HOL/Analysis/Operator_Norm.thy
changeset 71425 f2da99316b86
parent 70136 f03a01a18c6e
equal deleted inserted replaced
71424:e83fe2c31088 71425:f2da99316b86