src/HOL/ex/Lagrange.thy
changeset 21404 eb85850d3eb7
parent 20807 bd3b60f9a343
child 22173 7a78b9531b80
     1.1 --- a/src/HOL/ex/Lagrange.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/ex/Lagrange.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  theorem.  *}
     1.5  
     1.6  definition
     1.7 -  sq :: "'a::times => 'a"
     1.8 +  sq :: "'a::times => 'a" where
     1.9    "sq x == x*x"
    1.10  
    1.11  text {* The following lemma essentially shows that every natural