src/HOL/Typedef.thy
changeset 80482 2136ecf06a4c
parent 69913 ca515cf61651
child 81586 257f93d40d7c
equal deleted inserted replaced
80481:0e2b09fef3d2 80482:2136ecf06a4c