src/HOL/Record.thy
changeset 61045 c7a7f063704a
parent 60758 d8d85a8172b5
child 61799 4cf66f21b764