| changeset 4091 | 771b1f6422a8 |
| parent 2907 | 0e272e4c7cb2 |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/AxClasses/Group/GroupDefs.ML Mon Nov 03 12:22:43 1997 +0100 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML Mon Nov 03 12:24:13 1997 +0100 @@ -26,7 +26,7 @@ (* cartesian products *) -val prod_ss = simpset_of "Prod"; +val prod_ss = simpset_of Prod.thy; goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";