src/HOL/Analysis/Norm_Arith.thy
changeset 69133 22fe10b4c0c6
parent 68607 67bb59e49834
child 69517 dc20f278e8f3