src/HOL/Old_Number_Theory/Chinese.thy
changeset 57086 db7c735e963d
parent 56544 b60d5d119489
child 57492 74bf65a1910a
equal deleted inserted replaced
57085:cb212f52c2a3 57086:db7c735e963d