src/HOL/ex/Chinese.thy
changeset 63750 9c8a366778e1
parent 61343 5b5656a63bd6
equal deleted inserted replaced
63749:4fe8cfaeb1fc 63750:9c8a366778e1