src/HOL/Typedef.thy
changeset 61109 1c98bfc5d743
parent 61102 0ec9fd8d8119
child 61799 4cf66f21b764