src/HOL/NumberTheory/Chinese.thy
changeset 11295 66925f23ac7f
parent 11049 7eef34adb852
child 11468 02cd5d5bc497