src/HOL/Tools/old_primrec.ML
changeset 39775 e4c85d8c2aba
parent 39557 fe5722fce758