src/HOL/Import/HOL/prim_rec.imp
changeset 40148 8728165d366e
parent 35092 cfe605c54e50
child 44763 b50d5d694838