--- 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