src/HOL/Analysis/Operator_Norm.thy
changeset 69096 62a0d10386c1
parent 68833 fde093888c16
child 69518 bf88364c9e94
equal deleted inserted replaced
69083:6f8ae6ddc26b 69096:62a0d10386c1