src/HOL/Tools/typedef.ML
changeset 33002 f3f02f36a3e2
parent 32970 fbd2bb2489a8
child 33314 53d49370f7af