src/HOL/Library/Old_Recdef.thy
changeset 66805 274b4edca859
parent 60523 be2d9f5ddc76
child 67091 1393c2340eec
equal deleted inserted replaced
66804:3f9bb52082c4 66805:274b4edca859