src/HOL/Record.thy
changeset 81016 8e2114e6205b
parent 80934 8e72f55295fd
child 81125 ec121999a9cb