src/HOL/Number_Theory/UniqueFactorization.thy
changeset 54494 a220071f6708
parent 51548 757fa47af981
child 54611 31afce809794
equal deleted inserted replaced
54493:5b34a5b93ec2 54494:a220071f6708