src/HOL/Record.thy
changeset 9993 c0f7fb6e538e
parent 9729 40cfc3dd27da
child 10093 44584c2b512b