src/HOL/Record.thy
changeset 24705 8e77a023d080
parent 22817 9dfadec17cc4
child 25705 45a2ffc5911e
equal deleted inserted replaced
24704:9a95634ab135 24705:8e77a023d080