src/HOL/Library/Old_Recdef.thy
changeset 69298 360bde07daf9
parent 67091 1393c2340eec
child 69605 a96320074298
equal deleted inserted replaced
69297:4cf8a0432650 69298:360bde07daf9