src/HOL/Examples/Records.thy
changeset 76207 8fcbce9f317c
parent 76042 e076b1b42c44
child 78624 8d7394e533f8