src/HOL/Tools/recdef_package.ML
changeset 22277 b89dc456dbc6
parent 22101 6d13239d5f52
child 22360 26ead7ed4f4b