| changeset 42695 | a94ad372b2f5 |
| parent 41229 | d797baa3d57c |
| child 43311 | 1efdcb579b6c |
| 42694:30278eb9c9db | 42695:a94ad372b2f5 |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 header {* Extensible records with structural subtyping *} |
9 header {* Extensible records with structural subtyping *} |
10 |
10 |
11 theory Record |
11 theory Record |
12 imports Plain Quickcheck |
12 imports Plain Quickcheck_Exhaustive |
13 uses ("Tools/record.ML") |
13 uses ("Tools/record.ML") |
14 begin |
14 begin |
15 |
15 |
16 subsection {* Introduction *} |
16 subsection {* Introduction *} |
17 |
17 |