diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2009-09-05  John D. Ramsdell  <ramsdell@mitre.org>
+
+	* src/Algebra/AbelianGroup/UnificationMatching.hs:  Added
+	reference to Andrew Kennedy's Ph.D. thesis as in contains a proof
+	of correctness of the implemented matching algorithm.
+
 2009-08-29  John D. Ramsdell  <ramsdell@mitre.org>
 
 	* src/Algebra/AbelianGroup/UnificationMatching.hs (Substitution,
diff --git a/agum.cabal b/agum.cabal
--- a/agum.cabal
+++ b/agum.cabal
@@ -1,5 +1,5 @@
 Name:			agum
-Version:		2.0
+Version:		2.1
 Maintainer:		ramsdell@mitre.org
 Cabal-Version:		>= 1.2
 License:		GPL
@@ -14,7 +14,7 @@
 			Substitition s is more general than s\' if
 			there is a substitition s\" such that s\' =
 			s\" o s.
-Category:		Algebra.AbelianGroup
+Category:		Algebra
 Build-Type:		Simple
 Extra-Source-Files:	readme.txt ChangeLog Makefile
 
diff --git a/src/Algebra/AbelianGroup/UnificationMatching.hs b/src/Algebra/AbelianGroup/UnificationMatching.hs
--- a/src/Algebra/AbelianGroup/UnificationMatching.hs
+++ b/src/Algebra/AbelianGroup/UnificationMatching.hs
@@ -308,16 +308,13 @@
 --
 --     c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = 0
 --
--- where n is the length of c.  Otherwise, (c, d) represents a
--- sequence of inhomogeneous linear equations with the same
--- left-hand-side:
+-- where n is the length of c.  Otherwise, (c, d) represents the
+-- inhomogeneous equation:
 --
---     c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = d[0]
---     c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = d[1]
---     ...
---     c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = d[m-1]
+--     c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = g
 --
--- where m is the length of d.
+-- where g = gcd(d[0], d[1], ..., d[m-1]), and m is the length of d.
+-- Thus g is the greatest common denominator of the elements of d.
 
 type Subst = [(Int, LinEq)]
 
@@ -431,6 +428,12 @@
 divide :: Int -> [Int] -> [Int]
 divide small t =
     map (\x -> div x small) t
+
+-- Elementary Abelian group matching is equivalent to unification with
+-- constants.  A proof of correctness of this algorithm, cast as
+-- unification with constants, is in Chapter 3, Section 1 of
+-- "Programming Languages and Dimensions", Andrew Kennedy's
+-- Ph.D. thesis from St. Catharine's College in 1996.
 
 -- Input and Output