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