thys/rec_def.thy
changeset 146 0f52b971cc03
parent 70 2363eb91d9fd