src/HOL/Library/old_recdef.ML
changeset 61396 ce1b2234cab6
parent 61268 abe08fb15a12
child 61424 c3658c18b7bc