src/HOL/ex/Chinese.thy
changeset 81342 cfb165af55c5
parent 80914 d97fdabd9e2b