src/HOL/Record.thy
changeset 38566 8176107637ce
parent 38539 3be65f879bcd
child 41229 d797baa3d57c