thys/rec_def.thy
changeset 129 c3832c4963c4
parent 70 2363eb91d9fd