src/HOL/Tools/recdef.ML
changeset 59977 ad2d1cd53877
parent 59936 b8ffc3dc9e24
child 60364 fd5052b1881f
equal deleted inserted replaced
59976:046399298519 59977:ad2d1cd53877