src/HOL/Record.thy
changeset 9789 7e5e6c47c0b5
parent 9729 40cfc3dd27da
child 10093 44584c2b512b