src/HOL/Library/old_recdef.ML
changeset 61304 754e8ddbbc82
parent 61268 abe08fb15a12
child 61424 c3658c18b7bc