src/HOL/Typedef.thy
changeset 73888 9c2dd041477b
parent 69913 ca515cf61651
equal deleted inserted replaced
73884:0a12ca4f3e8d 73888:9c2dd041477b