equal
deleted
inserted
replaced
57 end |
57 end |
58 |
58 |
59 text {* \noindent Again, the interesting things enter the stage with |
59 text {* \noindent Again, the interesting things enter the stage with |
60 parametric types: *} |
60 parametric types: *} |
61 |
61 |
62 instantiation * :: (semigroup, semigroup) semigroup |
62 instantiation prod :: (semigroup, semigroup) semigroup |
63 begin |
63 begin |
64 |
64 |
65 instance proof |
65 instance proof |
66 fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup" |
66 fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup" |
67 show "p\<^isub>1 \<oplus> p\<^isub>2 \<oplus> p\<^isub>3 = p\<^isub>1 \<oplus> (p\<^isub>2 \<oplus> p\<^isub>3)" |
67 show "p\<^isub>1 \<oplus> p\<^isub>2 \<oplus> p\<^isub>3 = p\<^isub>1 \<oplus> (p\<^isub>2 \<oplus> p\<^isub>3)" |
110 specification of class operations and a non-trivial instance proof. |
110 specification of class operations and a non-trivial instance proof. |
111 |
111 |
112 This covers products as well: |
112 This covers products as well: |
113 *} |
113 *} |
114 |
114 |
115 instantiation * :: (monoidl, monoidl) monoidl |
115 instantiation prod :: (monoidl, monoidl) monoidl |
116 begin |
116 begin |
117 |
117 |
118 definition |
118 definition |
119 neutral_prod_def: "\<zero> = (\<zero>, \<zero>)" |
119 neutral_prod_def: "\<zero> = (\<zero>, \<zero>)" |
120 |
120 |