src/HOL/Typedef.thy
changeset 15900 d6156cb8dc2e
parent 15260 a12e999a0113
child 16417 9bc16273c2d4
equal deleted inserted replaced
15899:e30f9161890f 15900:d6156cb8dc2e