src/HOL/NumberTheory/Chinese.thy
changeset 23719 ccd9cb15c062
parent 23315 df3a7e9ebadb
child 23894 1a4167d761ac