src/HOL/Typedef.thy
changeset 15195 197e00ce3f20
parent 15140 322485b816ac
child 15260 a12e999a0113