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