src/HOL/Record.thy
changeset 48609 0090fab725e3
parent 47893 4cf901b1089a
child 48891 c0eafbd55de3