src/HOL/Tools/recdef.ML
changeset 45693 bbd2c7ffc02c
parent 45620 f2a587696afb
child 46185 afda84cd4d4b