src/HOL/Old_Number_Theory/Chinese.thy
changeset 59940 087d81f5213e
parent 59498 50b60f501b05
child 61382 efac889fccbc