# HG changeset patch
# User wenzelm
# Date 1196178517 -3600
# Node ID d5a382ccb5cc017a5d04c01c8d6d7745075bbd5f
# Parent  c41b433b0f6582ab9cd4436a4cc5a87d6a365570
challenge by John Harrison: down to 12s (was 17s, was 75s);

diff -r c41b433b0f65 -r d5a382ccb5cc src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Tue Nov 27 16:48:35 2007 +0100
+++ b/src/HOL/ex/Lagrange.thy	Tue Nov 27 16:48:37 2007 +0100
@@ -38,7 +38,7 @@
 by (simp add: sq_def ring_simps)
 
 
-text {* A challenge by John Harrison. Takes about 17s on a 1.6GHz machine. *}
+text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
 
 lemma fixes p1 :: "'a::comm_ring" shows
   "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *