src/HOL/Tools/typedef.ML
changeset 33326 7d0288d90535
parent 32970 fbd2bb2489a8
child 33314 53d49370f7af