src/HOL/Old_Number_Theory/Chinese.thy
changeset 57115 ae61587eb44a
parent 56544 b60d5d119489
child 57492 74bf65a1910a