src/HOL/Recdef.thy
changeset 43188 0c36ae874fcc
parent 39302 d7728f65b353
equal deleted inserted replaced
43187:95bd1ef1331a 43188:0c36ae874fcc