src/HOL/Tools/typedef.ML
changeset 33064 ba7ff3f9527a
parent 32970 fbd2bb2489a8
child 33314 53d49370f7af