src/HOL/Tools/recdef.ML
changeset 74594 2f28a0a758ab
parent 60520 09fc5eaa21ce