src/HOL/NumberTheory/Chinese.thy
changeset 21229 9c96c1ec235f
parent 20432 07ec57376051
child 21404 eb85850d3eb7