src/HOL/Record.thy
changeset 11582 f666c1e4133d
parent 11489 1fd5469c195e
child 11821 ad32c92435db