src/HOL/Record.thy
changeset 15298 a5bea99352d6
parent 15140 322485b816ac
child 16114 8d453f906e43
equal deleted inserted replaced
15297:0aff5d912422 15298:a5bea99352d6