src/HOL/Examples/Records.thy
changeset 81170 2d73c3287bd3
parent 80864 1b1f77bcee5f