changeset 43565 | a94ad372b2f5 |
parent 41495 | d797baa3d57c |
child 44182 | 1efdcb579b6c |
43564:30278eb9c9db | 43565: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 |