src/HOL/Old_Number_Theory/Chinese.thy
changeset 64281 bfc2e92d9b4c
parent 63167 0909deb8059b