src/HOL/Analysis/Operator_Norm.thy
changeset 69506 7d59af98af29
parent 68833 fde093888c16
child 69518 bf88364c9e94
equal deleted inserted replaced
69505:cc2d676d5395 69506:7d59af98af29