src/HOL/ex/Records.thy
changeset 46368 ded0390eceae
parent 46231 76e32c39dd43
child 47842 bfc08ce7b7b9