src/HOL/ex/Lagrange.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Lagrange.thy	Tue Nov 26 14:28:17 1996 +0100
@@ -0,0 +1,18 @@
+(*  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.
+
+The enterprising reader might consider proving all of Lagrange's thm.
+*)
+Lagrange = Ring +
+
+constdefs sq :: 'a::times => 'a
+         "sq x == x*x"
+
+end