src/HOL/Library/old_recdef.ML
changeset 61218 04c769fe1cb5
parent 61125 4c68426800de
child 61268 abe08fb15a12