changeset 31248 | d1c65a593daf |
parent 26932 | c398a3866082 |
child 31723 | f5cafe803b55 |
31247:71f163982a21 | 31248:d1c65a593daf |
---|---|
1 (* Title: HOL/ex/Records.thy |
1 (* Title: HOL/ex/Records.thy |
2 ID: $Id$ |
|
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, |
2 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, |
4 TU Muenchen |
3 TU Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header {* Using extensible records in HOL -- points and coloured points *} |
6 header {* Using extensible records in HOL -- points and coloured points *} |