src/HOL/Library/old_recdef.ML
changeset 61378 3e04c9ca001a
parent 61268 abe08fb15a12
child 61424 c3658c18b7bc