equal
deleted
inserted
replaced
5 This file is largely based on HOL/Finite_Set.thy. |
5 This file is largely based on HOL/Finite_Set.thy. |
6 *) |
6 *) |
7 |
7 |
8 header {* Product Operator for Commutative Monoids *} |
8 header {* Product Operator for Commutative Monoids *} |
9 |
9 |
10 theory FiniteProduct = Group: |
10 theory FiniteProduct imports Group begin |
11 |
11 |
12 text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not |
12 text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not |
13 possible, because here we have explicit typing rules like |
13 possible, because here we have explicit typing rules like |
14 @{text "x \<in> carrier G"}. We introduce an explicit argument for the domain |
14 @{text "x \<in> carrier G"}. We introduce an explicit argument for the domain |
15 @{text D}. *} |
15 @{text D}. *} |