| changeset 1266 | 3ae9fe3c0f68 |
| parent 1247 | 18b1441fb603 |
| child 1465 | 5d7a7e439cec |
--- a/src/HOL/AxClasses/Group/GroupDefs.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML Wed Oct 04 13:12:14 1995 +0100 @@ -29,6 +29,8 @@ (* cartesian products *) +val prod_ss = simpset_of "Prod"; + goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))"; by (simp_tac (prod_ss addsimps [assoc]) 1); qed "prod_assoc";