src/HOL/NumberTheory/Chinese.thy
changeset 29623 1219985d24b5
parent 27556 292098f2efdf
child 29948 cdf12a1cb963