src/HOL/ex/Chinese.thy
changeset 42078 d5bf0ce40bd7
parent 40967 5eb59b62e7de
child 58249 180f1b3508ed
equal deleted inserted replaced
42077:96c50a4210a2 42078:d5bf0ce40bd7