src/HOL/Analysis/L2_Norm.thy
changeset 69669 de2f0a24b0f0
parent 69600 86e8e7347ac0
child 69676 56acd449da41
equal deleted inserted replaced
69668:14a8cac10eac 69669:de2f0a24b0f0