equal
deleted
inserted
replaced
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 |
13 uses ("Tools/quickcheck_record.ML") ("Tools/record.ML") |
13 uses ("Tools/record.ML") |
14 begin |
14 begin |
15 |
15 |
16 subsection {* Introduction *} |
16 subsection {* Introduction *} |
17 |
17 |
18 text {* |
18 text {* |
450 "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
450 "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
451 |
451 |
452 |
452 |
453 subsection {* Record package *} |
453 subsection {* Record package *} |
454 |
454 |
455 use "Tools/quickcheck_record.ML" |
|
456 use "Tools/record.ML" setup Record.setup |
455 use "Tools/record.ML" setup Record.setup |
457 |
456 |
458 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
457 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
459 iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons |
458 iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons |
460 iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist |
459 iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist |