src/HOL/Library/Old_Recdef.thy
changeset 63414 beb987127d0f
parent 60523 be2d9f5ddc76
child 67091 1393c2340eec
equal deleted inserted replaced
63413:9fe2d9dc095e 63414:beb987127d0f