src/HOL/ex/Records.thy
changeset 12452 68493b92e7a6
parent 12266 fa0a3e95d395
child 12591 5a46569d2b05