src/HOL/Library/old_recdef.ML
changeset 61885 acdfc76a6c33
parent 61814 1ca1142e1711
child 62058 1cfd5d604937