src/HOL/ex/Chinese.thy
changeset 25985 8d69087f6a4b
parent 24312 bb5ec06f7c7a
child 39246 9e58f0499f57
equal deleted inserted replaced
25984:da0399c9ffcb 25985:8d69087f6a4b