src/HOL/Library/Old_Recdef.thy
changeset 53108 d84c8de81edf
parent 48891 c0eafbd55de3
child 55017 2df6ad1dbd66
equal deleted inserted replaced
53107:57c7294eac0a 53108:d84c8de81edf