src/HOL/Record.thy
changeset 40287 4af3706bcd5d
parent 38539 3be65f879bcd
child 41229 d797baa3d57c