src/HOL/Examples/Records.thy
changeset 79197 ad98105148e5
parent 78624 8d7394e533f8
child 80703 cc4ecaa8e96e