src/HOL/Tools/datatype_aux.ML
changeset 23811 b18557301bf9
parent 22596 d0d2af4db18f
child 24699 c6674504103f
equal deleted inserted replaced
23810:f5e6932d0500 23811:b18557301bf9