src/HOL/Tools/recdef.ML
changeset 45724 1f5fc44254d7
parent 45620 f2a587696afb
child 46185 afda84cd4d4b