# HG changeset patch
# User wenzelm
# Date 1237539152 -3600
# Node ID febd9234abdd8c6158d26a8d0c52d699dca842ec
# Parent  de241396389cf0b4ef02b9ce194854f98c6973dc
considerable speedup of benchmarks by using minimal simpset;

diff -r de241396389c -r febd9234abdd src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Fri Mar 20 09:51:41 2009 +0100
+++ b/src/HOL/ex/Lagrange.thy	Fri Mar 20 09:52:32 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Lagrange.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1996 TU Muenchen
 *)
@@ -35,7 +34,7 @@
    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 (simp add: sq_def algebra_simps)
+by (simp only: sq_def ring_simps)
 
 
 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
@@ -51,6 +50,6 @@
       sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
       sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-by (simp add: sq_def algebra_simps)
+by (simp only: sq_def ring_simps)
 
 end