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