src/HOL/Typedef.thy
changeset 24930 cc2e0e8c81af
parent 24269 4b2aac7669b3
child 25535 4975b7529a14
equal deleted inserted replaced
24929:408becab067e 24930:cc2e0e8c81af