src/HOL/NumberTheory/Chinese.thy
changeset 26732 6ea9de67e576
parent 23894 1a4167d761ac
child 27556 292098f2efdf