src/HOL/Old_Number_Theory/Chinese.thy
changeset 59898 81c70bdbd908
parent 59498 50b60f501b05
child 61382 efac889fccbc