src/HOL/Old_Number_Theory/Chinese.thy
changeset 56812 baef1c110f12
parent 56544 b60d5d119489
child 57492 74bf65a1910a