src/HOL/Tools/recdef_package.ML
changeset 16732 1bbe526a552c
parent 16646 666774b0d1b0
child 17057 0934ac31985f