src/HOL/Tools/recdef.ML
changeset 66826 0d60d2118544
parent 60520 09fc5eaa21ce
equal deleted inserted replaced
66825:9f6ec65f7a6e 66826:0d60d2118544