src/HOL/NumberTheory/Chinese.thy
changeset 12770 bdd17e7b5bd9
parent 11868 56db9f3a6b3e
child 13187 e5434b822a96