src/HOL/Tools/recdef_package.ML
changeset 11839 3ef83c265aca
parent 11740 86ac4189a1c1
child 12004 1703de633aaf