# HG changeset patch
# User ballarin
# Date 1039689228 -3600
# Node ID 550260ace09e13dc0fddd4f712d7a0bcd20f76c8
# Parent  a31e04831dd12171e3b5b5bea2311a29df4e5903
Fixed error that affected document preperation.

diff -r a31e04831dd1 -r 550260ace09e src/HOL/GroupTheory/Summation.thy
--- a/src/HOL/GroupTheory/Summation.thy	Wed Dec 11 10:12:48 2002 +0100
+++ b/src/HOL/GroupTheory/Summation.thy	Thu Dec 12 11:33:48 2002 +0100
@@ -4,6 +4,8 @@
     Copyright:  TU Muenchen
 *)
 
+header {* Summation Operator *}
+
 theory Summation = Group:
 
 (* Instantiation of LC from Finite_Set.thy is not possible,
@@ -54,7 +56,7 @@
   then show ?case ..
 qed
 
-subsubsection {* Left-commutative operations *}
+subsection {* Left-commutative operations *}
 
 locale LCD =
   fixes B :: "'b set"
@@ -235,7 +237,7 @@
 declare (in LCD)
   foldSetD_closed [rule del]
 
-subsubsection {* Commutative monoids *}
+subsection {* Commutative monoids *}
 
 text {*
   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
@@ -547,7 +549,7 @@
 
 text {*Usually, if this rule causes a failed congruence proof error,
    the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
-   Adding Pi_def to the simpset is often useful. *}
+   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
 
 declare funcsetI [rule del]
   funcset_mem [rule del]