diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Lagrange.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -17,7 +17,7 @@
 theorem.  *}
 
 definition
-  sq :: "'a::times => 'a"
+  sq :: "'a::times => 'a" where
   "sq x == x*x"
 
 text {* The following lemma essentially shows that every natural