src/HOL/ex/Records.thy
changeset 55147 bce3dbc11f95
parent 51717 9e7d1c139569
child 58249 180f1b3508ed
equal deleted inserted replaced
55146:525309c2e4ee 55147:bce3dbc11f95