src/HOL/ex/Chinese.thy
changeset 47850 c638127b4653
parent 40967 5eb59b62e7de
child 58249 180f1b3508ed
equal deleted inserted replaced
47849:48b52cdc214a 47850:c638127b4653