src/HOL/Analysis/L2_Norm.thy
changeset 68743 91162dd89571
parent 68607 67bb59e49834
child 69164 74f1b0f10b2b
equal deleted inserted replaced
68739:0c62e3b4f4c0 68743:91162dd89571