src/HOL/ex/Records.thy
changeset 48424 e6b0c14f04c8
parent 47842 bfc08ce7b7b9
child 51717 9e7d1c139569