src/HOL/Typedef.thy
changeset 29249 4dc278c8dc59
parent 29056 dc08e3990c77
child 29608 564ea783ace8
equal deleted inserted replaced
29248:f1f1bccf2fc5 29249:4dc278c8dc59