src/HOL/Tools/primrec.ML
changeset 38976 a4a465dc89d9
parent 38388 94d5624dd1f7
child 39288 f1ae2493d93f