src/HOL/Record.thy
changeset 61654 4a28eec739e9
parent 60758 d8d85a8172b5
child 61799 4cf66f21b764