src/HOL/Analysis/L2_Norm.thy
changeset 66759 918f15c9367a
parent 66453 cc19f7ca2ed6
child 67006 b1278ed3cd46