src/HOL/Old_Number_Theory/Chinese.thy
changeset 60299 5ae2a2e74c93
parent 59498 50b60f501b05
child 61382 efac889fccbc
equal deleted inserted replaced
60298:7c278b692aae 60299:5ae2a2e74c93