src/HOL/Typedef.thy
changeset 19579 b802d1804b77
parent 19459 2041d472fc17
child 20426 9ffea7a8b31c