src/HOL/Record.thy
changeset 6378 5780d71203bb
parent 5732 8712391bbf3d
child 7357 d0e16da40ea2