thys/rec_def.thy
changeset 150 3c504ca0ce95
parent 70 2363eb91d9fd