src/HOL/Analysis/Operator_Norm.thy
changeset 69506 7d59af98af29
parent 68833 fde093888c16
child 69518 bf88364c9e94