# HG changeset patch
# User paulson
# Date 1120753460 -7200
# Node ID a5ae2757dd09c694db0acff6d88ab3ca9bde0dbb
# Parent  9ffd706ae402187e4e3c66dee3784929e89b04a7
updated comment

diff -r 9ffd706ae402 -r a5ae2757dd09 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Thu Jul 07 18:22:01 2005 +0200
+++ b/src/HOL/ex/Lagrange.thy	Thu Jul 07 18:24:20 2005 +0200
@@ -34,8 +34,9 @@
 by(simp add: sq_def ring_eq_simps)
 
 
-(* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
+text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
 
+(*
 lemma "!!p1::'a::comm_ring.
  (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
  (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)