src/HOL/Typedef.thy
changeset 29108 12ca66b887a0
parent 28965 1de908189869
child 29056 dc08e3990c77