src/HOL/Record.thy
changeset 14352 a8b1a44d8264
parent 14080 9a50427d7165
child 14700 2f885b7e5ba7