src/HOL/ex/Chinese.thy
changeset 80917 2a77bc3b4eac
parent 80914 d97fdabd9e2b