src/HOL/Library/old_recdef.ML
changeset 70915 bd4d37edfee4
parent 70308 7f568724d67e
child 71179 592e2afdd50c