src/HOL/datatype.ML
changeset 3718 d78cf498a88c
parent 3615 e5322197cfea
child 3768 67f4ac759100
equal deleted inserted replaced
3717:e28553315355 3718:d78cf498a88c