src/HOL/Tools/recdef_package.ML
changeset 30518 07b45c1aa788
parent 30364 577edc39b501
child 30528 7173bf123335