--- a/src/HOL/ex/Lagrange.thy Wed Jun 13 16:29:51 2001 +0200
+++ b/src/HOL/ex/Lagrange.thy Wed Jun 13 16:30:12 2001 +0200
@@ -1,14 +1,14 @@
-(* Title: HOL/Integ/Lagrange.thy
+(* Title: HOL/ex/Lagrange.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1996 TU Muenchen
-This theory only contains a single thm, which is a lemma in Lagrange's proof
-that every natural number is the sum of 4 squares. It's sole purpose is to
-demonstrate ordered rewriting for commutative rings.
+This theory only contains a single theorem, which is a lemma in Lagrange's
+proof that every natural number is the sum of 4 squares. Its sole purpose is
+to demonstrate ordered rewriting for commutative rings.
-The enterprising reader might consider proving all of Lagrange's thm.
+The enterprising reader might consider proving all of Lagrange's theorem.
*)
Lagrange = Ring +