equal
deleted
inserted
replaced
6 |
6 |
7 theory Representable |
7 theory Representable |
8 imports Algebraic Universal Ssum Sprod One Fixrec |
8 imports Algebraic Universal Ssum Sprod One Fixrec |
9 uses |
9 uses |
10 ("Tools/repdef.ML") |
10 ("Tools/repdef.ML") |
11 ("Tools/holcf_library.ML") |
|
12 ("Tools/Domain/domain_take_proofs.ML") |
11 ("Tools/Domain/domain_take_proofs.ML") |
13 ("Tools/Domain/domain_isomorphism.ML") |
12 ("Tools/Domain/domain_isomorphism.ML") |
14 begin |
13 begin |
15 |
14 |
16 subsection {* Class of representable types *} |
15 subsection {* Class of representable types *} |
776 apply (simp add: u_map_map) |
775 apply (simp add: u_map_map) |
777 done |
776 done |
778 |
777 |
779 subsection {* Constructing Domain Isomorphisms *} |
778 subsection {* Constructing Domain Isomorphisms *} |
780 |
779 |
781 use "Tools/holcf_library.ML" |
|
782 use "Tools/Domain/domain_take_proofs.ML" |
780 use "Tools/Domain/domain_take_proofs.ML" |
783 use "Tools/Domain/domain_isomorphism.ML" |
781 use "Tools/Domain/domain_isomorphism.ML" |
784 |
782 |
785 setup {* |
783 setup {* |
786 fold Domain_Isomorphism.add_type_constructor |
784 fold Domain_Isomorphism.add_type_constructor |