src/HOL/Algebra/FiniteProduct.thy
changeset 14706 71590b7733b7
parent 14666 65f8680c3f16
child 14750 8f1ee65bd3ea
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,11 +1,11 @@
     1.4 -(*  Title:      Product Operator for Commutative Monoids
     1.5 +(*  Title:      HOL/Algebra/FiniteProduct.thy
     1.6      ID:         $Id$
     1.7      Author:     Clemens Ballarin, started 19 November 2002
     1.8  
     1.9  This file is largely based on HOL/Finite_Set.thy.
    1.10  *)
    1.11  
    1.12 -header {* Product Operator *}
    1.13 +header {* Product Operator for Commutative Monoids *}
    1.14  
    1.15  theory FiniteProduct = Group:
    1.16