src/HOL/Analysis/Norm_Arith.thy
changeset 65083 9a0e34edfad1
parent 63928 d81fb5b46a5c
child 66453 cc19f7ca2ed6