equal
deleted
inserted
replaced
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_Narrowing |
12 imports Plain Quickcheck_Narrowing |
13 keywords "record" :: thy_decl |
13 keywords "record" :: thy_decl |
14 uses ("Tools/record.ML") |
|
15 begin |
14 begin |
16 |
15 |
17 subsection {* Introduction *} |
16 subsection {* Introduction *} |
18 |
17 |
19 text {* |
18 text {* |
459 "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
458 "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
460 |
459 |
461 |
460 |
462 subsection {* Record package *} |
461 subsection {* Record package *} |
463 |
462 |
464 use "Tools/record.ML" setup Record.setup |
463 ML_file "Tools/record.ML" setup Record.setup |
465 |
464 |
466 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
465 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd |
467 iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons |
466 iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons |
468 iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist |
467 iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist |
469 iso_tuple_update_accessor_eq_assist tuple_iso_tuple |
468 iso_tuple_update_accessor_eq_assist tuple_iso_tuple |