src/HOL/Library/old_recdef.ML
changeset 61829 55c85d25e18c
parent 61814 1ca1142e1711
child 62058 1cfd5d604937
equal deleted inserted replaced
61828:2d89fa0b3ff6 61829:55c85d25e18c