src/HOL/Record.thy
changeset 14377 f454b3004f8f
parent 14080 9a50427d7165
child 14700 2f885b7e5ba7