src/HOL/Typedef.thy
changeset 23290 c358025ad8db
parent 23247 b99dce43d252
child 23433 c2c10abd2a1e