src/HOL/Tools/recdef_package.ML
changeset 12395 d6913de7655f
parent 12371 80ca9058db95
child 12448 473cb9f9e237