src/HOL/Typedef.thy
changeset 32887 85e7ab9020ba
parent 31723 f5cafe803b55
child 37863 7f113caabcf4
equal deleted inserted replaced
32886:aba29da80c1b 32887:85e7ab9020ba