src/HOL/NumberTheory/Chinese.thy
changeset 26589 43cb72871897
parent 23894 1a4167d761ac
child 27556 292098f2efdf