src/HOL/Tools/recdef.ML
changeset 78394 761d12b043d0
parent 60520 09fc5eaa21ce