src/HOL/NumberTheory/Chinese.thy
changeset 22330 00ca68f5ce29
parent 21404 eb85850d3eb7
child 23315 df3a7e9ebadb