src/HOL/Record.thy
changeset 9738 2e1dca5af2d4
parent 9729 40cfc3dd27da
child 10093 44584c2b512b