src/HOL/Tools/recdef.ML
changeset 57418 6ab1c7cb0b8d
parent 56249 0fda98dd2c93
child 57964 3dfc1bf3ac3d