src/HOL/Analysis/Operator_Norm.thy
changeset 71699 8e5c20e4e11a
parent 70136 f03a01a18c6e
equal deleted inserted replaced
71698:b69dc6bcbea3 71699:8e5c20e4e11a