src/HOL/Library/Old_Recdef.thy
changeset 68384 4a3fc3420747
parent 67091 1393c2340eec
child 69605 a96320074298
equal deleted inserted replaced
68383:93a42bd62ede 68384:4a3fc3420747