src/HOL/Analysis/Operator_Norm.thy
changeset 69096 62a0d10386c1
parent 68833 fde093888c16
child 69518 bf88364c9e94