src/HOL/Old_Number_Theory/Chinese.thy
changeset 44371 3a10392fb8c3
parent 39159 0dec18004e75
child 44766 d4d33a4d7548
equal deleted inserted replaced
44370:03d91bfad83b 44371:3a10392fb8c3