src/HOL/Old_Number_Theory/Chinese.thy
changeset 32749 3282c12a856c
parent 32479 521cc9bf2958
child 38159 e9b4835a54ee
equal deleted inserted replaced
32748:887c68b70f7d 32749:3282c12a856c