src/HOL/Library/Old_Recdef.thy
changeset 68658 16cc1161ad7f
parent 67091 1393c2340eec
child 69605 a96320074298