src/HOL/Record.thy
changeset 32777 8ae3a48c69d9
parent 32764 690f9cccf232
child 32799 7478ea535416