src/HOL/Record.thy
changeset 39214 49fc6c842d6c
parent 38539 3be65f879bcd
child 41229 d797baa3d57c