src/HOL/Library/Old_Recdef.thy
changeset 68575 d40d03487f64
parent 67091 1393c2340eec
child 69605 a96320074298
equal deleted inserted replaced
68571:2a6e258bfd66 68575:d40d03487f64