src/HOL/Tools/recdef_package.ML
changeset 9502 50ec59aff389
parent 8734 b456aba346a6
child 9640 8c6cf4f01644