src/HOL/ex/Chinese.thy
changeset 81271 fb391ad09b3c
parent 80914 d97fdabd9e2b
equal deleted inserted replaced
81270:b98595f82a88 81271:fb391ad09b3c