src/HOL/ex/Lagrange.thy
changeset 58776 95e58e04e534
parent 37885 c43805c80eb6
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/ex/Lagrange.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4     sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
     1.5     sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
     1.6     sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
     1.7 -by (simp only: sq_def field_simps)
     1.8 +by (simp only: sq_def algebra_simps)
     1.9  
    1.10  
    1.11  text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    1.12 @@ -44,6 +44,6 @@
    1.13        sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    1.14        sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    1.15        sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    1.16 -by (simp only: sq_def field_simps)
    1.17 +by (simp only: sq_def algebra_simps)
    1.18  
    1.19  end