src/HOL/Old_Number_Theory/Chinese.thy
changeset 38795 848be46708dc
parent 38159 e9b4835a54ee
child 39159 0dec18004e75