src/HOL/Record.thy
changeset 48546 f81cf2fcd3a0
parent 47893 4cf901b1089a
child 48891 c0eafbd55de3