src/HOL/Library/old_recdef.ML
changeset 61829 55c85d25e18c
parent 61814 1ca1142e1711
child 62058 1cfd5d604937