src/HOL/Tools/datatype_aux.ML
changeset 18532 0347c1bba406
parent 18377 0e1d025d57b3
child 18728 6790126ab5f6
equal deleted inserted replaced
18531:ce7b80b7c84e 18532:0347c1bba406