src/HOL/Nitpick_Examples/Record_Nits.thy
changeset 82407 fcc0f74ac086
parent 74641 6f801e1073fa