src/HOL/Record.thy
changeset 39100 e9467adb8b52
parent 38539 3be65f879bcd
child 41229 d797baa3d57c