src/HOL/Record.thy
changeset 80946 b76f64d7d493
parent 80934 8e72f55295fd
child 81125 ec121999a9cb