src/HOL/Tools/recdef_package.ML
changeset 20335 b5eca86ef9cc
parent 20291 c82b667b6dcc
child 21078 101aefd61aac