src/HOL/Analysis/Norm_Arith.thy
changeset 64362 8a0fe5469ba0
parent 63928 d81fb5b46a5c
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
64361:07d910a58a14 64362:8a0fe5469ba0