src/HOL/Tools/recdef.ML
changeset 60201 90e88e521e0e
parent 59936 b8ffc3dc9e24
child 60364 fd5052b1881f
equal deleted inserted replaced
60200:02fd729f2883 60201:90e88e521e0e