src/HOL/ex/Records.thy
changeset 27885 76b51cd0a37c
parent 26932 c398a3866082
child 31248 d1c65a593daf