src/HOL/NumberTheory/Chinese.thy
changeset 26462 dac4e2bce00d
parent 23894 1a4167d761ac
child 27556 292098f2efdf