src/HOL/Analysis/Norm_Arith.thy
changeset 69099 d44cb8a3e5e0
parent 68607 67bb59e49834
child 69517 dc20f278e8f3