src/HOL/Library/old_recdef.ML
changeset 60651 1049f3724ac0
parent 60642 48dd1cefb4ae
child 60699 7bf560b196a3
equal deleted inserted replaced
60650:40eef52464f3 60651:1049f3724ac0