equal
deleted
inserted
replaced
3 Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
3 Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
4 |
4 |
5 Extensible records with structural subtyping in HOL. |
5 Extensible records with structural subtyping in HOL. |
6 |
6 |
7 TODO: |
7 TODO: |
8 - field types: typedef; |
8 - field types: datatype; |
9 - operations and theorems: split, split_all/ex, ...; |
9 - operations and theorems: split, split_all/ex, ...; |
10 - field constructor: more specific type for snd component (x_more etc. classes); |
10 - field constructor: more specific type for snd component (x_more etc. classes); |
11 *) |
11 *) |
12 |
12 |
13 signature RECORD_PACKAGE = |
13 signature RECORD_PACKAGE = |