src/HOL/Library/Old_Recdef.thy
changeset 68593 d32d40d03e0a
parent 67091 1393c2340eec
child 69605 a96320074298
equal deleted inserted replaced
68589:9258f16d68b4 68593:d32d40d03e0a