src/HOL/ex/Records.thy
changeset 28605 12d6087ec18c
parent 26932 c398a3866082
child 31248 d1c65a593daf
equal deleted inserted replaced
28604:f36496b73227 28605:12d6087ec18c