src/HOL/Typedef.thy
changeset 23388 77645da0db85
parent 23247 b99dce43d252
child 23433 c2c10abd2a1e