src/HOL/Tools/recdef.ML
changeset 79755 3066125a7f51
parent 60520 09fc5eaa21ce