src/HOL/Record.thy
changeset 43310 d1265a4d8ae1
parent 42695 a94ad372b2f5
child 43311 1efdcb579b6c