src/HOL/Record.thy
changeset 34972 cc1d4c3ca9db
parent 34151 8d57ce46b3f7
child 35132 d137efecf793