src/HOL/Tools/recdef.ML
changeset 59977 ad2d1cd53877
parent 59936 b8ffc3dc9e24
child 60364 fd5052b1881f