src/HOL/ex/Chinese.thy
changeset 63750 9c8a366778e1
parent 61343 5b5656a63bd6