src/HOL/Library/old_recdef.ML
changeset 61943 7fba644ed827
parent 61814 1ca1142e1711
child 62058 1cfd5d604937
equal deleted inserted replaced
61942:f02b26f7d39d 61943:7fba644ed827