src/HOL/ex/Records.thy
changeset 15761 c9561302c74a
parent 15010 72fbe711e414
child 16417 9bc16273c2d4