src/HOL/Analysis/Operator_Norm.thy
changeset 68798 07714b60f653
parent 67685 bdff8bf0a75b
child 68833 fde093888c16
equal deleted inserted replaced
68794:63e84bd8e1f6 68798:07714b60f653