src/HOL/Record.thy
changeset 48487 94a9650f79fb
parent 47893 4cf901b1089a
child 48891 c0eafbd55de3