diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Lagrange.ML
--- a/src/HOL/ex/Lagrange.ML	Fri Nov 29 15:07:27 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/ex/Lagrange.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1996 TU Muenchen
-
-
-The following lemma schows that all composite natural numbers are sums of
-fours squares, provided all prime numbers are.
-*)
-
-goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
-\  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
-\  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
-\  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
-\  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
-\  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
-by(cring_simp 1);
-qed "Lagrange_lemma";