src/HOL/Number_Theory/UniqueFactorization.thy
changeset 54757 4960647932ec
parent 54611 31afce809794
child 55130 70db8d380d62
equal deleted inserted replaced
54756:dd0f4d265730 54757:4960647932ec