src/HOL/Old_Number_Theory/Chinese.thy
changeset 62199 fc55a4e3f439
parent 61382 efac889fccbc
child 63167 0909deb8059b