src/HOL/ex/Records.thy
changeset 47358 26c4e431ef05
parent 46231 76e32c39dd43
child 47842 bfc08ce7b7b9